merge of '6dbd04de03e12a60f6719db5199c0a399d2c1279'
authorHenning Heinold <heinold@inf.fu-berlin.de>
Sat, 19 Jul 2008 13:59:55 +0000 (13:59 +0000)
committerHenning Heinold <heinold@inf.fu-berlin.de>
Sat, 19 Jul 2008 13:59:55 +0000 (13:59 +0000)
     and 'be3713b5fac2aae7f226418a48c1d67f2f902170'


Trivial merge