etc/settings
changeset 72309 564012e31db1
parent 72193 742d94015918
child 72314 684f14b1e7fc
--- a/etc/settings	Sat Sep 26 11:43:25 2020 +0200
+++ b/etc/settings	Sat Sep 26 14:29:46 2020 +0200
@@ -59,14 +59,12 @@
 ### Document preparation (cf. isabelle latex/document)
 ###
 
-ISABELLE_LATEX="latex -file-line-error"
 ISABELLE_PDFLATEX="pdflatex -file-line-error"
 ISABELLE_BIBTEX="bibtex"
 ISABELLE_MAKEINDEX="makeindex"
 ISABELLE_EPSTOPDF="epstopdf"
 
 if [ "$ISABELLE_PLATFORM_FAMILY" = "windows" ]; then
-  ISABELLE_LATEX="latex -c-style-errors"
   ISABELLE_PDFLATEX="pdflatex -c-style-errors"
 fi
 
@@ -140,7 +138,6 @@
 esac
 
 PDF_VIEWER="$ISABELLE_OPEN"
-DVI_VIEWER="$ISABELLE_OPEN"
 
 
 ###