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="$?"