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.