# HG changeset patch
# User wenzelm
# Date 1456347804 -3600
# Node ID 36e885190439a222868d809db59d1db8f363e39c
# Parent  a4b68bf18f8d34af345c48607d5254ba588a870a
tuned signature;

diff -r a4b68bf18f8d -r 36e885190439 src/Pure/Concurrent/bash.scala
--- a/src/Pure/Concurrent/bash.scala	Wed Feb 24 16:00:57 2016 +0000
+++ b/src/Pure/Concurrent/bash.scala	Wed Feb 24 22:03:24 2016 +0100
@@ -23,10 +23,13 @@
     def error(s: String, err_rc: Int = 0): Result =
       copy(err_lines = err_lines ::: List(s), rc = rc max err_rc)
 
+    def ok: Boolean = rc == 0
+    def interrupted: Boolean = rc == Exn.Interrupt.return_code
+
     def check: Result =
-      if (rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
-      else if (rc != 0) Library.error(err)
-      else this
+      if (ok) this
+      else if (interrupted) throw Exn.Interrupt()
+      else Library.error(err)
 
     def print: Result =
     {
diff -r a4b68bf18f8d -r 36e885190439 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Feb 24 16:00:57 2016 +0000
+++ b/src/Pure/Tools/build.scala	Wed Feb 24 22:03:24 2016 +0100
@@ -632,7 +632,7 @@
     {
       val res = result.join
 
-      if (res.rc == 0 && !is_pure(name))
+      if (res.ok && !is_pure(name))
         Present.finish(progress, browser_info, graph_file, info, name)
 
       graph_file.delete
@@ -858,7 +858,7 @@
             progress.echo(res.err)
 
             val heap =
-              if (res.rc == 0) {
+              if (res.ok) {
                 (output_dir + log(name)).file.delete
 
                 val sources = make_stamp(name)