changeset 10194 | f6dfed43561d |
parent 9766 | da6788606f54 |
child 10209 | b24210573eca |
--- a/src/Pure/ML-Systems/polyml-4.0.ML Wed Oct 11 19:06:36 2000 +0200 +++ b/src/Pure/ML-Systems/polyml-4.0.ML Thu Oct 12 11:47:17 2000 +0200 @@ -121,7 +121,8 @@ in fun mask_interrupt f = change_signal Signal.SIG_IGN f; -fun exhibit_interrupt f = change_signal Signal.SIG_DFL f; +fun exhibit_interrupt f = + change_signal (Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())) f; end;