Allow user packages in 'make doc'

[mtorpey]

make doc fails if there is no installation of GAPDoc in gap/pkg/ because it runs with the -r flag that disables user package directories.

This PR removes the -r flag so that user-installed GAPDoc and other packages can be used in compiling the doc.

This is the last link required for users to be able to do a complete install using only PackageManager and no other packages.

(I have some déjà vu with this – apologies if we've talked about this before and I've forgotten.)

[fingolfin]

Seems fine to me, but it would be good if e.g. @ThomasBreuer and @frankluebeck also had a quick look / think about this.

[ThomasBreuer]

I had added the -r flag in #5835.
My point was that calling make_doc is intended to run w.r.t. the currently distributed GAP packages, and the user specific root directory likely provides newer package versions. (For example, my directory contains the development version of GAPDoc.)

[ThomasBreuer]

I do not understand the statement

This is the last link required for users to be able to do a complete install using only PackageManager and no other packages.

Is the idea to install GAP without all packages, then install PackageManager, and then let PackageManager install all other packages (on demand?) in the user specific root directory?

[mtorpey]

That's the idea, yes. I don't know whether most users would want to set up GAP this way, but it could be a useful style of bootstrapping a working system. I seem to remember this ambition was why InstallRequiredPackages was requested.

The instructions here show how to do this as a complete process, and I'm hoping they'll now be successful.

[ThomasBreuer]

Thanks @mtorpey.

A disadvantage of installing GAP with all its packages in the user specific root directory is that one cannot install two different GAP versions (with corresponding packages) this way, because there is just one user specific root directory for all GAP versions.