#include <stdio.h>
#include "spinix.h"
int main (int argc, char **argv)
{
spinix_enter();
printf("Hello World!\n");
spinix_exit(0);
}