merge of '11752201b0467d112cbc4a2fd6b4e3bafa1a66a2'
authorHenning Heinold <heinold@inf.fu-berlin.de>
Wed, 13 Aug 2008 21:03:19 +0000 (21:03 +0000)
committerHenning Heinold <heinold@inf.fu-berlin.de>
Wed, 13 Aug 2008 21:03:19 +0000 (21:03 +0000)
     and '461b0f25ec4df76026bbc143ddf9a76a9690fd9e'


Trivial merge