------- Comment #8 from dominiq at lps dot ens dot fr 2008-02-04 11:26 ------- > Wow, that was weird...
Yes, it was! > Hardware glitch? May be, our DHCP server at home did "funny" things during the week-end (apparently it did not cope well with a new machine(?)). Could also be my own "hardware". Thanks for having looked at the problem. -- http://gcc.gnu.org/bugzilla/show_bug.cgi?id=35068