GitLab

There are a few inconsistencies with the hadrian vs make bindists which I will document here and then we can decide if we do anything about them.

• hadrian puts docs in docs rather than doc.
• hadrian puts the pdf documentation in a pdfs folder but make puts the pdfs in the doc folder (one level up)
• hadrian calls the Haddock html documentation Haddock, which is consistent with the output name (as declared by utils/haddock/doc/conf.py) but make puts it in a folder called haddock (lower case).

At the moment in !7679 (closed) I modified distrib/mkDocs/mkDocs to just look in the right places in the hadrian bindist.