merge of '8a346ac0cb1c268bff470b0f2784075ba7eaea0b'
authorHenning Heinold <heinold@inf.fu-berlin.de>
Wed, 4 Jun 2008 10:24:28 +0000 (10:24 +0000)
committerHenning Heinold <heinold@inf.fu-berlin.de>
Wed, 4 Jun 2008 10:24:28 +0000 (10:24 +0000)
     and '9dee7a8725dc7dc8f9882b09eee3fe13e9ab8eac'


Trivial merge