lib/Tools/latex
changeset 73730 2f023b2b0e1e
parent 73728 dfc7579aae9d
--- a/lib/Tools/latex	Tue May 18 17:02:45 2021 +0200
+++ b/lib/Tools/latex	Tue May 18 17:19:19 2021 +0200
@@ -80,9 +80,6 @@
     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