1. 22 Jun, 2018 1 commit
    • giannozz's avatar
      Added compiled documentation files in *.pdf. *txt, *html format. · ae635622
      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)