equal
deleted
inserted
replaced
78 TEXINPUTS="$ISABELLE_HOME/lib/texinputs:$TEXINPUTS" |
78 TEXINPUTS="$ISABELLE_HOME/lib/texinputs:$TEXINPUTS" |
79 ISABELLE_LATEX="latex" |
79 ISABELLE_LATEX="latex" |
80 ISABELLE_PDFLATEX="pdflatex" |
80 ISABELLE_PDFLATEX="pdflatex" |
81 ISABELLE_BIBTEX="bibtex" |
81 ISABELLE_BIBTEX="bibtex" |
82 ISABELLE_DVIPS="dvips -D 600" |
82 ISABELLE_DVIPS="dvips -D 600" |
|
83 ISABELLE_EPSTOPDF="epstopdf" |
83 |
84 |
84 # Paranoia setting ... |
85 # Paranoia setting ... |
85 #unset TEXMF |
86 #unset TEXMF |
86 |
87 |
87 # The thumbpdf tool is probably not generally available ... |
88 # The thumbpdf tool is probably not generally available ... |