Improved documentation handling

[ludo@gnu.org (Ludovic Courtès)]

I just committed two new build phases to ‘core-updates’:

  • The ‘validate-documentation-location’ phase renames, if needed,
    ‘man’ to ‘share/man’ and ‘info’ to ‘share/info’.

  • The ‘compress-documentation’ phase compresses man pages and Info
    files with gzip, as per
    <https://www.debian.org/doc/debian-policy/ch-docs.html> (the nice
    thing being that we can implement the policy instead of just writing
    it down.  ;-))

As an example, the ‘share/info’ directory in libc is down from 4.3 MiB
to 1 MiB.

Hydra is building it now, we’ll see if it needs more tweaking.

As usual, comments welcome!

Ludo’.