merge of '0032a5aa8024f5f2c529e386ce8e631cbe32131e'
authorHenning Heinold <heinold@inf.fu-berlin.de>
Fri, 25 Jul 2008 15:47:54 +0000 (15:47 +0000)
committerHenning Heinold <heinold@inf.fu-berlin.de>
Fri, 25 Jul 2008 15:47:54 +0000 (15:47 +0000)
     and '0948ccadfd54691007037bfcc956a41728ab914d'


Trivial merge