| changeset 7776 | 8fd408765c1d |
| parent 7773 | ce86227f29d0 |
| child 7813 | 4412debd3004 |
--- a/etc/settings Thu Oct 07 12:36:53 1999 +0200 +++ b/etc/settings Thu Oct 07 12:37:55 1999 +0200 @@ -55,10 +55,6 @@ ### 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"