# HG changeset patch
# User wenzelm
# Date 1495789756 -7200
# Node ID 9a28fc03c3fefaf022550f057a33a1642e953a9b
# Parent  de3adcf6a276acc00817ba78d05c0db7cd482c1d
tuned signature;

diff -r de3adcf6a276 -r 9a28fc03c3fe src/Pure/Admin/other_isabelle.scala
--- a/src/Pure/Admin/other_isabelle.scala	Thu May 25 21:59:53 2017 +0200
+++ b/src/Pure/Admin/other_isabelle.scala	Fri May 26 11:09:16 2017 +0200
@@ -14,12 +14,20 @@
 
   /* static system */
 
-  def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
+  def bash(
+      script: String,
+      redirect: Boolean = false,
+      echo: Boolean = false,
+      strict: Boolean = true): Process_Result =
     progress.bash(Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script,
-      env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo)
+      env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo, strict = strict)
 
-  def apply(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
-    bash("bin/isabelle " + cmdline, redirect, echo)
+  def apply(
+      cmdline: String,
+      redirect: Boolean = false,
+      echo: Boolean = false,
+      strict: Boolean = true): Process_Result =
+    bash("bin/isabelle " + cmdline, redirect = redirect, echo = echo, strict = strict)
 
   def resolve_components(echo: Boolean): Unit =
     other_isabelle("components -a", redirect = true, echo = echo).check
diff -r de3adcf6a276 -r 9a28fc03c3fe src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Thu May 25 21:59:53 2017 +0200
+++ b/src/Pure/System/progress.scala	Fri May 26 11:09:16 2017 +0200
@@ -29,11 +29,13 @@
     cwd: JFile = null,
     env: Map[String, String] = Isabelle_System.settings(),
     redirect: Boolean = false,
-    echo: Boolean = false): Process_Result =
+    echo: Boolean = false,
+    strict: Boolean = true): Process_Result =
   {
     Isabelle_System.bash(script, cwd = cwd, env = env, redirect = redirect,
       progress_stdout = echo_if(echo, _),
-      progress_stderr = echo_if(echo, _))
+      progress_stderr = echo_if(echo, _),
+      strict = strict)
   }
 }