@@ -0,0 +1,4 @@
+#ifndef EXTRA_FLAG
+syntax error EXTRA_FLAG should be defined on the command line for this file
+#endif
+int ALLOK;