Skip to content
  • 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)
    ae635622