install default_handler for SIGINT initially as well;
authorwenzelm
Thu, 12 Oct 2000 17:54:22 +0200
changeset 10209 b24210573eca
parent 10208 2b284ef75049
child 10210 e8aa81362f41
install default_handler for SIGINT initially as well;
src/Pure/ML-Systems/polyml-4.0.ML
--- 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;