#include <stdio.h>
#include <stdarg.h>

void mach_print(const char *);

#ifndef EXTERNAL_MACH_PRINT
asm (".global mach_print;"
     " mach_print:;"
     " mov $0xffffffe2, %eax;"
     " lcall $0x7, $0x0;"
     " ret;");
#endif /* EXTERNAL_MACH_PRINT */

#define BUFFER_SIZE 1024
static void
mach_printf(const char *format, ...)
{
  va_list ap;
  char buf[BUFFER_SIZE];

  va_start(ap, format);
  vsnprintf(buf, sizeof(buf), format, ap);
  mach_print(buf);
  va_end(ap);
}