# 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