0f1e1628dd
Now all 64 bit binaries work, and I tested that we did not break the 32 bit ones XXX: That 0x80000000 seems wrong for 64 bit stuff.