#include <acpi.h>

#include <acclib.h>

extern void AcpiOsPrint(const char *str);

void AcpiOsPrintf(const char *format, ...) {
  va_list args;
  va_start(args, format);
  AcpiOsVprintf(format, args);
  va_end(args);
}
void AcpiOsVprintf(const char *format, va_list args) {
  char buffer[4096];
  vsnprintf(buffer, 4096, format, args);
  AcpiOsPrint(buffer);
}