Fix applying style settings to online GAP documentation

[slel]

If I visit

https://www.gap-system.org/Manuals/doc/ref/chap0.html

I can click "[Style]" which takes me to

https://www.gap-system.org/Manuals/doc/ref/chooser.html?BACK=https:///Manuals/doc/ref/chap0.html

which has something wrong for the "BACK=..." part of the url,
in which the base site was ignored. Indeed, if I now select
"Times/serif" and click "Apply settings to last page", I get

https://manuals/doc/ref/chap0.html?GAPDocStyle=times

instead of

https://www.gap-system.org/Manuals/doc/ref/chap0.html?GAPDocStyle=times

[wilfwilson]

Thanks for the report @slel. This is caused by a bug in GAPDoc, which I reported in frankluebeck/GAPDoc#46 and which a fix has been developed that will appear in the next GAPDoc release.

This problem (I think) affects all manuals of GAP and GAP packages that were built with a version of GAPDoc that does not contain the fix in frankluebeck/GAPDoc#46; each such manual needs a line adding to its manual.js file.

I have manually made this fix to the GAP manuals, which I presume are the most-used manuals on the GAP website. Therefore the specific problem that you reported is now fixed.

I have not done the same for package manuals, which also suffer from the same problem. For package, I think it is best for wait for the next GAPDoc to be released, and then for each package to make a new release that includes the fixed manual.js, and then for a GAP release to be made that includes all of these packages. Only then will the problem be fully resolved; this might never happen.

[fingolfin]

Actually, why shouldn't we just update the manual.js files for all package manuals hosted on gap-system.org? Granted, it's a temporary measure only, but I see now downside?

[wilfwilson]

Yes we could do that, and perhaps (for now) update the etc/extract-manuals.py script to do it in the future, too.

[fingolfin]

I've manually updated all manual.js files to the latest version now.

If we modify etc/extract_manuals.py to modify, I'd copy the version from GAPDoc to all other packages, to ensure they all have the latest at all time.

[fingolfin]

A fixed version of GAPDoc has been shipping since GAP 4.12.0 (released August 2022), so any package released since then should be fixed.

There are almost 50 packages released before that date, though not all of them use GAPDoc.

So it would still be useful to enhance etc/extract_manuals.py to update all manual.js files as sketched above.