#ifndef EXTRA_FLAG
syntax error EXTRA_FLAG should be defined on the command line for this file
#endif
int ALLOK;