Revision 160079

Move the config for the users manual to extra/.
Yes, this means you need to know how to edit the config
in order to learn how to edit the config.  But you already
need to know how to start and install the server before
you can get to the manual.

Most people should probably be using alternative documentation
forms anyway (online, off-browsable single-language tarballs,
windows help, etc).

Also, clean up a few comments in the extra config section.