[build] Avoid using awk to format build ID as hexadecimal

[build] Avoid using awk to format build ID as hexadecimal

The version of awk used in FreeBSD seems to be incapable of formatting
unsigned 32-bit integers above 0x80000000 and will silently render any
such value as 0x80000000.  For example:

  echo 3735928559 | awk '{printf "0x%08x", $1}'

will produce 0x80000000 instead of the correct 0xdeadbeef.

This results in an approximately 50% chance of a build ID collision
when building on FreeBSD.

Work around this problem by passing the decimal value directly in the
ld --defsym argument value.

Signed-off-by: Michael Brown <mcb30@ipxe.org>