# HG changeset patch
# User wenzelm
# Date 1621347319 -7200
# Node ID 2574de12ad2918c42b8c9670fe060be298baa9da
# Parent  aa7662e475b6e309eaf194891e72abd97aedbdce
clarified command-line options;

diff -r aa7662e475b6 -r 2574de12ad29 etc/settings
--- a/etc/settings	Tue May 18 16:01:01 2021 +0200
+++ b/etc/settings	Tue May 18 16:15:19 2021 +0200
@@ -65,12 +65,12 @@
 ###
 
 if [ "$ISABELLE_PLATFORM_FAMILY" = "windows" ]; then
-  ISABELLE_PDFLATEX="pdflatex -c-style-errors"
+  ISABELLE_PDFLATEX="pdflatex -interaction=nonstopmode -c-style-errors"
 else
-  ISABELLE_PDFLATEX="pdflatex -file-line-error"
+  ISABELLE_PDFLATEX="pdflatex -interaction=nonstopmode -file-line-error"
 fi
 
-ISABELLE_LUALATEX="lualatex --file-line-error"
+ISABELLE_LUALATEX="lualatex --interaction=nonstopmode --file-line-error"
 ISABELLE_BIBTEX="bibtex"
 ISABELLE_MAKEINDEX="makeindex"
 ISABELLE_EPSTOPDF="epstopdf"
diff -r aa7662e475b6 -r 2574de12ad29 lib/Tools/latex
--- a/lib/Tools/latex	Tue May 18 16:01:01 2021 +0200
+++ b/lib/Tools/latex	Tue May 18 16:15:19 2021 +0200
@@ -70,7 +70,7 @@
 
 # operations
 
-function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
+function run_pdflatex () { $ISABELLE_PDFLATEX "$FILEBASE.tex"; }
 function run_bibtex () {
   $ISABELLE_BIBTEX </dev/null "$FILEBASE"
   RC="$?"