Merge branch 'master' into HEAD
authorChristoph Junghans <junghans@mpip-mainz.mpg.de>
Thu, 26 Aug 2010 09:41:20 +0000 (11:41 +0200)
committerChristoph Junghans <junghans@mpip-mainz.mpg.de>
Thu, 26 Aug 2010 09:41:20 +0000 (11:41 +0200)
commit80d4ec447025cdfbaac9e3f0ce1954dbcce2b894
treeb0c3ab473b2e8a0eb26b7fdb8f322caaf59592e8
parent5f46e60d93f223b0e4ed4e496fe6613f2749ff56
parentfd3d76d87b32ddf7e7e3a197733bd28a2c9f430d
Merge branch 'master' into HEAD