tuned --- more robust;
authorwenzelm
Tue, 18 May 2021 19:59:22 +0200
changeset 73988 9b77e267e6a9
parent 73987 a1ef2589c33f
child 73989 b13b2c1d419e
tuned --- more robust;
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()))
       }
     }