# HG changeset patch
# User wenzelm
# Date 939292675 -7200
# Node ID 8fd408765c1da4f882c2148602f94c3a2f1949df
# Parent  26898fbd19ca3c6e3ec57500d87181a02b637b98
removed TeX environment hacking;

diff -r 26898fbd19ca -r 8fd408765c1d etc/settings
--- 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"