Commit 720183ac2fe427922000f321d27856eb42160ad8

Bruno Haible 2007-07-06T22:56:38

Shut up a makeinfo warning.