Commit 6d03958a046c6783210c538dd9f656553434a804

Bruno Haible 2008-06-04T22:10:07

Undo last commit, as it does not solve the problem entirely.