[BUG] Help not found in Docker

[ProgramComputer]

Help not found when clicked on when running on Docker and causes error.

[HugoFara]

Hi there, I thought a bit about the issue and its implications. Here are the main aspects:

• docs/ is 14 MB of dead weight as I don't think the full documentation is necessary for most users.
• docs/info.html is referenced everywhere as the "all documentation in one file" element.
• The automatic documentation (docs/*/) is 13.5 MB.

As long as we ignore the folders in docs, the overhead stays under control and the documentation is partially accessible. In the worst case a Docker user needs the full documentation in his container, it is still possible to regenerate it.

Could you modify your pull request by ignoring the folders only?