merge of '087653573b61d9d8b527394ed24c5b05ccae172d'
authorHenning Heinold <heinold@inf.fu-berlin.de>
Sat, 28 Jul 2007 16:49:03 +0000 (16:49 +0000)
committerHenning Heinold <heinold@inf.fu-berlin.de>
Sat, 28 Jul 2007 16:49:03 +0000 (16:49 +0000)
     and 'c9de0582a3606aa3fe61a814739480c3cafe40d5'


Trivial merge