Since github and gitlab just distribute a snapshot of the git repository,
these files must be in the repository as well. NOTA BENE:
All changes MUST GO TO *.tex or *.def FILES, NOT to these files!
Also note that the "make doc" machinery produces also *.xml files and
latex2html converted html versions of latex files. I don't think they belong
to the repository (latex files should maybe be replaced by md files)