more informative bibtex errors;
authorwenzelm
Mon, 31 Aug 2020 16:48:31 +0200
changeset 72461 4710dd5093a3
parent 72460 0881bc2c607d
child 72462 6b620d91e8cc
more informative bibtex errors;
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 ()
 {