merge of '5ae815d03c9ef1f749d3938f74dbd8e73c455921'
authorHenning Heinold <heinold@inf.fu-berlin.de>
Sat, 26 Jul 2008 20:29:41 +0000 (20:29 +0000)
committerHenning Heinold <heinold@inf.fu-berlin.de>
Sat, 26 Jul 2008 20:29:41 +0000 (20:29 +0000)
     and '8a3d387dc07aa9256e0f2ed81a4e1c1242fdfa6e'


Trivial merge