+ static const char *hdr = "# Game options\n# ------------\n"
+ "# Lines starting with '#' are comments. Options set to their default value are\n"
+ "# automatically commented when this file is written. If you want to change some\n"
+ "# option, make sure to remove the '#' from the beginning of the line, or your\n"
+ "# change will have no effect.\n";
+