Small hack to get the right value of $prefix into config.h. If no

prefix is specified on the command line the value of $prefix when the
config.h is generated is 'NONE' instead of '/usr/testbed', so we have
to manually define it to the default ourselves.