We don't actually have a stdio.h header file. Our printf() functions are

defined in vsprintf.h.  (This may change, since vsprintf.h is a
non-standard name, but for now it's the one to use.)

There should be no need to include vsprintf.h just for DBG() statements,
since include/compiler.h forces it in for a debug build anyway.

src/interface/pxe/pxe_loader.c

@@ -22,7 +22,6 @@
  * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
  */
 
-#include <stdio.h>
 #include "pxe.h"
 
 /* PXENV_UNDI_LOADER

src/interface/pxe/pxe_tftp.c

@@ -22,7 +22,6 @@
  * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
  */
 
-#include <stdio.h>
 #include "pxe.h"
 
 static int pxe_tftp_read_block ( unsigned char *data, unsigned int block,

src/interface/pxe/pxe_udp.c

@@ -4,7 +4,6 @@
  *
  */
 
-#include <stdio.h>
 #include <string.h>
 #include <byteswap.h>
 #include <gpxe/udp.h>

src/interface/pxe/pxe_undi.c

@@ -22,7 +22,6 @@
  * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
  */
 
-#include <stdio.h>
 #include "pxe.h"
 
 /* PXENV_UNDI_STARTUP