merge of 'ac7218640853632ccf63747d5222d3db90378a56'
authorHenning Heinold <heinold@inf.fu-berlin.de>
Wed, 30 Jul 2008 19:50:18 +0000 (19:50 +0000)
committerHenning Heinold <heinold@inf.fu-berlin.de>
Wed, 30 Jul 2008 19:50:18 +0000 (19:50 +0000)
     and 'e82644f718a3dd0995659c6a5818c83ebc731f8e'


Trivial merge