# HG changeset patch
# User wenzelm
# Date 1621360762 -7200
# Node ID 9b77e267e6a97abdaa85dc10ce4cee639ada404f
# Parent  a1ef2589c33f03bf6ad1f6ffd7c60501d8c83da8
tuned --- more robust;

diff -r a1ef2589c33f -r 9b77e267e6a9 src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Tue May 18 19:49:06 2021 +0200
+++ b/src/Pure/Thy/document_build.scala	Tue May 18 19:59:22 2021 +0200
@@ -344,12 +344,18 @@
         def latex_bash(fmt: String = "pdf", ext: String = "tex"): String =
           "isabelle latex -o " + Bash.string(fmt) + " " + root_bash(ext)
 
-        List(
-          latex_bash(),
-          "{ [ ! -f " + root_bash("bib") + " ] || " + latex_bash("bbl") + "; }",
-          "{ [ ! -f " + root_bash("idx") + " ] || " + latex_bash("idx") + "; }",
-          latex_bash(),
-          latex_bash()).mkString(" && ")
+        cat_lines(
+          List(
+            "set -e",
+            latex_bash(),
+            "if [ -f " + root_bash("bib") + " ]; then",
+            "  " + latex_bash("bbl"),
+            "fi",
+            "if [ -f " + root_bash("idx") + " ]; then",
+            "  " + latex_bash("idx"),
+            "fi",
+            latex_bash(),
+            latex_bash()))
       }
     }