improved exhibit_interrupt;

--- 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;