merge of '55132066284089ca5853bcbb50bbd4990ec25823'
authorHenning Heinold <heinold@inf.fu-berlin.de>
Wed, 6 Aug 2008 15:14:45 +0000 (15:14 +0000)
committerHenning Heinold <heinold@inf.fu-berlin.de>
Wed, 6 Aug 2008 15:14:45 +0000 (15:14 +0000)
     and '5565cda387e227c33c34f8743f541e7737fc5b1b'


Trivial merge