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)

Trivial merge