o Don't rely on particular features of awk (apparently, the parsing of
  hex numbers only works in mawk, but not others).
Should fix #1