src/Pure/Tools/build.scala
changeset 56667 65e84b0ef974
parent 56533 cd8b6d849b6a
child 56668 56335a8e2e8b
     1.1 --- a/src/Pure/Tools/build.scala	Wed Apr 23 11:40:42 2014 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Wed Apr 23 12:39:23 2014 +0200
     1.3 @@ -605,7 +605,7 @@
     1.4        args_file.delete
     1.5        timer.map(_.cancel())
     1.6  
     1.7 -      if (res.rc == 130) {
     1.8 +      if (res.rc == Exn.Interrupt.return_code) {
     1.9          if (timeout) res.add_err("*** Timeout").set_rc(1)
    1.10          else res.add_err("*** Interrupt")
    1.11        }
    1.12 @@ -832,7 +832,7 @@
    1.13  
    1.14                  File.write(output_dir + log(name), Library.terminate_lines(res.out_lines))
    1.15                  progress.echo(name + " FAILED")
    1.16 -                if (res.rc != 130) {
    1.17 +                if (res.rc != Exn.Interrupt.return_code) {
    1.18                    progress.echo("(see also " + (output_dir + log(name)).file.toString + ")")
    1.19                    val lines = res.out_lines.filterNot(_.startsWith("\f"))
    1.20                    val tail = lines.drop(lines.length - 20 max 0)