[SeaBIOS] [PATCH 21/31] output.c: Make printf() capable to print 64bit int values