# HG changeset patch
# User wenzelm
# Date 1598885311 -7200
# Node ID 4710dd5093a35d206f15e32d3b0d992145636847
# Parent  0881bc2c607d51e3b2d30e207b0c8a69ee578126
more informative bibtex errors;

diff -r 0881bc2c607d -r 4710dd5093a3 lib/Tools/latex
--- 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 ()
 {