--- a/lib/Tools/document	Fri Dec 08 23:43:58 2017 +0100
+++ b/lib/Tools/document	Sun Dec 10 14:29:14 2017 +0100
@@ -137,7 +137,9 @@
     RC="$?"
   fi
 
-  if [ "$RC" -eq 0 -a -f "$ROOT_NAME.$OUTFORMAT" ]; then
+  if [ "$RC" -ne 0 ]; then
+    isabelle latex_errors -n "$ROOT_NAME"
+  elif [ -f "$ROOT_NAME.$OUTFORMAT" ]; then
     cp -f "$ROOT_NAME.$OUTFORMAT" "../$NAME.$OUTFORMAT"
   fi