src/Pure/System/bash.scala
changeset 71684 5036edb025b7
parent 71601 97ccf48c2f0c
child 71705 7b75d52a1bf1
equal deleted inserted replaced
71683:fd487d261169 71684:5036edb025b7
   113       var running = true
   113       var running = true
   114       var count = 10
   114       var count = 10
   115       while (running && count > 0) {
   115       while (running && count > 0) {
   116         if (kill(signal)) {
   116         if (kill(signal)) {
   117           Exn.Interrupt.postpone {
   117           Exn.Interrupt.postpone {
   118             Thread.sleep(100)
   118             Time.seconds(0.1).sleep
   119             count -= 1
   119             count -= 1
   120           }
   120           }
   121         }
   121         }
   122         else running = false
   122         else running = false
   123       }
   123       }