It was broken when we changed write_config() to
  remove the symbols it wrote to config.h

They are redundant at best and misleading if you
change the type.