fileno() is a mess on some operating systems. Don't
deliberately convert between FILE * and file handles.
Change-Id: I5be62a731f928333ea2e5843d81f541453fdb396
Signed-off-by: Stefan Reinauer <stefan.reinauer@coreboot.org>
Reviewed-on: http://review.coreboot.org/11636
Tested-by: build bot (Jenkins)
Reviewed-by: Alexandru Gagniuc <mr.nuke.me@gmail.com>
1bb487c474