[SeaBIOS] [PATCH] scripts: Allow encodeint.py to take integers in hex notation.