Merging 7971:887db7d64bc9 with 7970:21b063622472.
authorPeter Molnar <pm@complang.tuwien.ac.at>
Wed, 19 Mar 2008 12:07:59 +0000 (13:07 +0100)
committerPeter Molnar <pm@complang.tuwien.ac.at>
Wed, 19 Mar 2008 12:07:59 +0000 (13:07 +0100)

Trivial merge