--- a/lib/Tools/latex Sun Aug 30 21:21:04 2020 +0100
+++ b/lib/Tools/latex Mon Aug 31 16:48:31 2020 +0200
@@ -72,7 +72,14 @@
function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
-function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
+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"; }
function copy_styles ()
{