diff --git a/lib/Tools/latex b/lib/Tools/latex
--- a/lib/Tools/latex
+++ b/lib/Tools/latex
@@ -1,116 +1,123 @@
 #!/usr/bin/env bash
 #
 # Author: Markus Wenzel, TU Muenchen
 #
 # DESCRIPTION: run LaTeX (and related tools)
 
 
 PRG="$(basename "$0")"
 
 function usage()
 {
   echo
   echo "Usage: isabelle $PRG [OPTIONS] [FILE]"
   echo
   echo "  Options are:"
   echo "    -o FORMAT    specify output format: pdf (default), dvi, bbl, idx, sty"
   echo
   echo "  Run LaTeX (and related tools) on FILE (default root.tex),"
   echo "  producing the specified output format."
   echo
   exit 1
 }
 
 function fail()
 {
   echo "$1" >&2
   exit 2
 }
 
 
 ## process command line
 
 # options
 
 OUTFORMAT=pdf
 
 while getopts "o:" OPT
 do
   case "$OPT" in
     o)
       OUTFORMAT="$OPTARG"
       ;;
     \?)
       usage
       ;;
   esac
 done
 
 shift $(($OPTIND - 1))
 
 
 # args
 
 FILE="root.tex"
 [ "$#" -ge 1 ] && { FILE="$1"; shift; }
 
 [ "$#" -ne 0 ] && usage
 
 
 ## main
 
 # root file
 
 DIR="$(dirname "$FILE")"
 FILEBASE="$(basename "$FILE" .tex)"
 [ "$DIR" = . ] || FILEBASE="$DIR/$FILEBASE"
 
 function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; }
 
 
 # operations
 
 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 ()
 {
   for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty
   do
     TARGET="$DIR"/$(basename "$STYLEFILE")
     perl -p -e 's/\$[I]d:?(?:\s)*([^\$]*)\$//g' "$STYLEFILE" > "$TARGET"
   done
 }
 
 case "$OUTFORMAT" in
   pdf)
     check_root && \
     run_pdflatex
     RC="$?"
     ;;
   dvi)
     check_root && \
     run_latex
     RC="$?"
     ;;
   bbl)
     check_root && \
     run_bibtex
     RC="$?"
     ;;
   idx)
     check_root && \
     run_makeindex
     RC="$?"
     ;;
   sty)
     copy_styles
     RC="$?"
     ;;
   *)
     fail "Bad output format '$OUTFORMAT'"
     ;;
 esac
 
 exit "$RC"