#include <unistd.h>
#include <stdarg.h>
#include <sys/syscall.h>
#include <stdio.h>

int vsprintf(char *buf, const char *fmt, va_list args);

/* Write a formatted string to stdout */
int
printf(const char *fmt, ...)
{
	int len;
	char buf[8196];
	va_list args;
	va_start(args, fmt);
	len = vsprintf(buf, fmt, args);
	va_end(args);

	len = write(STDOUT_FILENO, buf, len);
	return len;
}