diff -r 2574de12ad29 -r dfc7579aae9d lib/Tools/latex
--- a/lib/Tools/latex	Tue May 18 16:15:19 2021 +0200
+++ b/lib/Tools/latex	Tue May 18 16:18:39 2021 +0200
@@ -70,31 +70,23 @@
 
 # operations
 
-function run_pdflatex () { $ISABELLE_PDFLATEX "$FILEBASE.tex"; }
-function run_bibtex () {
-  $ISABELLE_BIBTEX </dev/null "$FILEBASE"
-  RC="$?"
-  if [ "$RC" -gt 0 -a -f "${FILEBASE}.blg" ]; then
-    perl -n -e 'if (m/^I (found no.*$)/) { print "bibtex $1\n"; }' "${FILEBASE}.blg" >&2
-  fi
-  return "$RC"
-}
-function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }
-
 case "$OUTFORMAT" in
   pdf)
-    check_root && \
-    run_pdflatex
+    check_root
+    $ISABELLE_PDFLATEX "$FILEBASE.tex"
     RC="$?"
     ;;
   bbl)
-    check_root && \
-    run_bibtex
+    check_root
+    $ISABELLE_BIBTEX </dev/null "$FILEBASE"
     RC="$?"
+    if [ "$RC" -gt 0 -a -f "${FILEBASE}.blg" ]; then
+      perl -n -e 'if (m/^I (found no.*$)/) { print "bibtex $1\n"; }' "${FILEBASE}.blg" >&2
+    fi
     ;;
   idx)
-    check_root && \
-    run_makeindex
+    check_root
+    $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"
     RC="$?"
     ;;
   *)