Document preparation setup;
authorwenzelm
Thu, 07 Oct 1999 12:33:54 +0200
changeset 7773 ce86227f29d0
parent 7772 c7b2f68c79fb
child 7774 6da9b544a12d
Document preparation setup;
etc/settings
--- 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
 ###