------- Additional Comments From schnetter at aei dot mpg dot de 2005-09-26 02:09 ------- Thank you for the hint.
On my system there is /usr/bin/awk, which calls itself "awk version 20040207", and there is /sw/bin/ awk, which is GNU awk 3.1.4. The latter comes first in my path. The file "Makefile" in the same directory as the bad file "options.h" contains the line "AWK = gawk". When I execute the command gawk -f /Users/eschnett/src/gcc/gcc/opt-functions.awk -f /Users/eschnett/src/gcc/gcc/opth- gen.awk < optionlist in the directory where the bad file "options.h" is generated, the output is the same -- there is a spurious minus sign. The /usr/bin/awk produces the correct output. It seems that this version of GNU awk is then somehow broken. I'll try to install a different one via fink. -- http://gcc.gnu.org/bugzilla/show_bug.cgi?id=24062
