src/Pure/Tools/build.scala
changeset 62399 36e885190439
parent 62303 f868f12f9419
child 62400 833af0d6d469
     1.1 --- a/src/Pure/Tools/build.scala	Wed Feb 24 16:00:57 2016 +0000
     1.2 +++ b/src/Pure/Tools/build.scala	Wed Feb 24 22:03:24 2016 +0100
     1.3 @@ -632,7 +632,7 @@
     1.4      {
     1.5        val res = result.join
     1.6  
     1.7 -      if (res.rc == 0 && !is_pure(name))
     1.8 +      if (res.ok && !is_pure(name))
     1.9          Present.finish(progress, browser_info, graph_file, info, name)
    1.10  
    1.11        graph_file.delete
    1.12 @@ -858,7 +858,7 @@
    1.13              progress.echo(res.err)
    1.14  
    1.15              val heap =
    1.16 -              if (res.rc == 0) {
    1.17 +              if (res.ok) {
    1.18                  (output_dir + log(name)).file.delete
    1.19  
    1.20                  val sources = make_stamp(name)