Commit c580832d28bc3e7f2b9701375685f118244c0f6e

Bruno Haible 2007-10-21T14:20:08

Update after move from cvs to git.