-
giannozz authored
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)
ae635622