Hello again, I investigated against various sources at gnu.org. The bug exists at least in versions 8.5 to 8.9, and was corrected in version 8.10, probably by chance during implementation of output formatting extensions.
Hence the problem comes from debian-squeeze using an old release, and this issue can be closed, as far as I am concerned. Thanks for taking the time to test it anyway. Jean-Pierre
