equal
deleted
inserted
replaced
59 ISABELLE_LATEX="latex" |
59 ISABELLE_LATEX="latex" |
60 ISABELLE_PDFLATEX="pdflatex" |
60 ISABELLE_PDFLATEX="pdflatex" |
61 ISABELLE_BIBTEX="bibtex" |
61 ISABELLE_BIBTEX="bibtex" |
62 ISABELLE_DVIPS="dvips -D 600" |
62 ISABELLE_DVIPS="dvips -D 600" |
63 |
63 |
64 # The thumpdf tool is probably not generally available ... |
64 # The thumbpdf tool is probably not generally available ... |
65 #ISABELLE_THUMBPDF="thumbpdf" |
65 #ISABELLE_THUMBPDF="thumbpdf" |
66 |
66 |
67 |
67 |
68 ### |
68 ### |
69 ### Misc path settings |
69 ### Misc path settings |