--- a/src/Pure/ML-Systems/polyml-4.0.ML Thu Oct 12 17:52:44 2000 +0200
+++ b/src/Pure/ML-Systems/polyml-4.0.ML Thu Oct 12 17:54:22 2000 +0200
@@ -118,11 +118,14 @@
val _ = Signal.signal (sig_int, old_handler);
in release result end;
+val default_handler = Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ());
+
in
+val _ = Signal.signal (sig_int, default_handler);
+
fun mask_interrupt f = change_signal Signal.SIG_IGN f;
-fun exhibit_interrupt f =
- change_signal (Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())) f;
+fun exhibit_interrupt f = change_signal default_handler f;
end;