improved exhibit_interrupt;
authorwenzelm
Thu Oct 12 11:47:17 2000 +0200 (2000-10-12)
changeset 10194f6dfed43561d
parent 10193 1d6ae1ef8e64
child 10195 325b6279ae4f
improved exhibit_interrupt;
src/Pure/ML-Systems/polyml-4.0.ML
     1.1 --- a/src/Pure/ML-Systems/polyml-4.0.ML	Wed Oct 11 19:06:36 2000 +0200
     1.2 +++ b/src/Pure/ML-Systems/polyml-4.0.ML	Thu Oct 12 11:47:17 2000 +0200
     1.3 @@ -121,7 +121,8 @@
     1.4  in
     1.5  
     1.6  fun mask_interrupt f = change_signal Signal.SIG_IGN f;
     1.7 -fun exhibit_interrupt f = change_signal Signal.SIG_DFL f;
     1.8 +fun exhibit_interrupt f =
     1.9 +  change_signal (Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())) f;
    1.10  
    1.11  end;
    1.12