Unicode bug in my gawk for Windows 3.1.3

[Brian Williams]

I love gawk, and was delightfully surprised to find that it is sort of
Unicode-compliant.
 
However, I run gawk -f < unicodefile.txt > unicodefile2.txt --
 
 -- this generates unicodefile2.txt as a Unicode file (which you'd
expect)
 -- the line endings are messed up -- it looks like the print statements
replace every '\n' single byte with '\r\n' as 2 bytes, which in Unicode
on Windows is incorrect.
 
I tried to get around by using printf :
  printf("some string \x0D\x00\x0A\x00") 
 
but this produces a line ending that looks like 0D 00 0D 0A 00 00
instead of 0D 00 0A 00
 
The darn program is too "smart" for it's own good!