merge of '816810f6dfc46f435b5ae83e81e9cb7eab296ef8'
authorHenning Heinold <heinold@inf.fu-berlin.de>
Sat, 7 Jul 2007 13:39:43 +0000 (13:39 +0000)
committerHenning Heinold <heinold@inf.fu-berlin.de>
Sat, 7 Jul 2007 13:39:43 +0000 (13:39 +0000)
     and 'eeb734a87c690a455488894bd874c0c20ada064b'


Trivial merge