merge of '8ad08e33aab6e79d2f20645f27087e958b0aa2c7'
authorHenning Heinold <heinold@inf.fu-berlin.de>
Thu, 24 Jul 2008 13:46:21 +0000 (13:46 +0000)
committerHenning Heinold <heinold@inf.fu-berlin.de>
Thu, 24 Jul 2008 13:46:21 +0000 (13:46 +0000)
     and 'bd0863efd4fd5edcafb9afbb746e0525af04d455'


Trivial merge