Commit d3546315684435f31c4d95e26ead751aaa8ea7e8

Bruno Haible 2008-12-21T11:31:43

Oops, remove unintended commit.