--- 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 =
{
--- 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)