src/Pure/Tools/build.scala
changeset 68331 7eaaa8f48331
parent 68305 5321218147d3
child 68486 6984a55f3cba
     1.1 --- a/src/Pure/Tools/build.scala	Wed May 30 14:34:43 2018 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Wed May 30 14:46:04 2018 +0200
     1.3 @@ -836,10 +836,8 @@
     1.4          system_mode = system_mode, sessions = List(logic)).ok) 0
     1.5      else {
     1.6        progress.echo("Build started for Isabelle/" + logic + " ...")
     1.7 -      progress.interrupt_handler {
     1.8 -        Build.build(options, progress = progress, build_heap = build_heap, dirs = dirs,
     1.9 -          system_mode = system_mode, sessions = List(logic)).rc
    1.10 -      }
    1.11 +      Build.build(options, progress = progress, build_heap = build_heap, dirs = dirs,
    1.12 +        system_mode = system_mode, sessions = List(logic)).rc
    1.13      }
    1.14    }
    1.15  }