changeset 7773 | ce86227f29d0 |
parent 7762 | c98d70538033 |
child 7776 | 8fd408765c1d |
--- a/etc/settings Thu Oct 07 12:27:44 1999 +0200 +++ b/etc/settings Thu Oct 07 12:33:54 1999 +0200 @@ -52,6 +52,20 @@ ### +### Document preparation +### + +#TeX environment hacking (for teTeX) +unset TEXMF +PATH="/usr/local/tetex-1.0/bin:$PATH" + +TEXINPUTS="$ISABELLE_HOME/lib/texinputs:$TEXINPUTS" +ISABELLE_LATEX="latex" +ISABELLE_PDFLATEX="pdflatex" +ISABELLE_DVIPS="dvips -D 600" + + +### ### Misc path settings ###