merge of '9fd082bd3a6b033c885925024d8f350d1b0c0438'
authorHenning Heinold <heinold@inf.fu-berlin.de>
Tue, 24 Jul 2007 20:35:54 +0000 (20:35 +0000)
committerHenning Heinold <heinold@inf.fu-berlin.de>
Tue, 24 Jul 2007 20:35:54 +0000 (20:35 +0000)
     and 'b9e4925c1b541f575dbfe4e254451b986acf1d60'


Trivial merge