#include <stdio.h>
#include "spinix.h"

int main (int argc,  char **argv)
{
    spinix_enter();
    printf("Hello World!\n");
    spinix_exit(0);
}