/* Dieser Text wird vernuenftig formatiert */
       int main(void)
       {
          printf("Hello, World!");
          return 0;
       }