Move manuals to separate subdomain, e.g. docs.gap-system.org

[fingolfin]

Rationale: like the content of files.gap-system.org, the manuals are big and not stored on github. By moving them to a separate subdomain, we gain flexibility, eg www, docs and files could in principle be served by different machines.

[fingolfin]

I've set this up in principle:

• for GAP manuals, e.g.
  • https://www.gap-system.org/Manuals/doc/ref/chap0.html
  • https://docs.gap-system.org/doc/ref/chap0.html
• for packages, e.g.
  • https://www.gap-system.org/Manuals/pkg/ace/htm/chapters.htm
  • https://docs.gap-system.org/pkg/ace/htm/chapters.htm
• or also
  • https://www.gap-system.org/Manuals/pkg/automata/doc/chap0.html
  • https://docs.gap-system.org/pkg/automata/doc/chap0.html

So right now, both of these work.

Next would be to have the former redirect to the latter, and then update all our links to reference the new addresses.

[fingolfin]

I've now also arranged it so that we have a crude versioning scheme going on:

• https://docs.gap-system.org/v4.11.1/doc/ref/chap0.html
• https://docs.gap-system.org/v4.12.0/doc/ref/chap0.html

Both work and deliver what one might expect... and https://docs.gap-system.org/doc/ref/chap0.html still works. Internally this is for now just a symlink to v4.12.0; it could be turned into a redirect instead; that way bookmarks would end up referencing the URL with a specific version in it, which I think is "better".

Much more could be done with regards to versioning the manuals (e.g. for packages), but I'll try not to get sidetracked too much here.

[fingolfin]

I have now enabled the redirects, so that all manual links now redirect to the separate subdomain.