# HG changeset patch
# User wenzelm
# Date 1010594178 -3600
# Node ID a44fd835df98bb6ad10f2556cb5cc7bfa8397407
# Parent  2b0aa746e4b822f86d1f61d7f9161fb97ee2fa79
removed TEXINPUTS;

diff -r 2b0aa746e4b8 -r a44fd835df98 etc/settings
--- a/etc/settings	Wed Jan 09 14:44:24 2002 +0100
+++ b/etc/settings	Wed Jan 09 17:36:18 2002 +0100
@@ -75,7 +75,6 @@
 ### Document preparation
 ###
 
-TEXINPUTS="$ISABELLE_HOME/lib/texinputs:$TEXINPUTS"
 ISABELLE_LATEX="latex"
 ISABELLE_PDFLATEX="pdflatex"
 ISABELLE_BIBTEX="bibtex"