# HG changeset patch
# User wenzelm
# Date 1532805686 -7200
# Node ID 71aa5a9128c21cc7faf95f2969077ddd7b5c1118
# Parent  2e31887d96647509807d0fcd17967a7a87c0dc4c
proper return code (true) if file is absent;

diff -r 2e31887d9664 -r 71aa5a9128c2 src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Sat Jul 28 19:55:14 2018 +0200
+++ b/src/Pure/Thy/present.scala	Sat Jul 28 21:21:26 2018 +0200
@@ -277,8 +277,8 @@
         "Failed to build document in " + File.path(dir.absolute_file))
     }
 
-    bash("[ -f " + root_bash(document_format) + " ] && cp -f " +
-      root_bash(document_format) + " " + File.bash_path(document_target)).check
+    bash("if [ -f " + root_bash(document_format) + " ]; then cp -f " +
+      root_bash(document_format) + " " + File.bash_path(document_target) + "; fi").check
   }