merge of '79b32dd15f1426dc8a2c0f2fea8b3e6caefff570'
authorHenning Heinold <heinold@inf.fu-berlin.de>
Mon, 2 Jun 2008 21:36:39 +0000 (21:36 +0000)
committerHenning Heinold <heinold@inf.fu-berlin.de>
Mon, 2 Jun 2008 21:36:39 +0000 (21:36 +0000)
     and 'd0dad3c0880bea593e98565689d54952ead355ab'


Trivial merge