# HG changeset patch
# User wenzelm
# Date 971366062 -7200
# Node ID b24210573eca9135dd2eaa52fd36a66803c053a7
# Parent  2b284ef75049b241dd87770ebd2d5bab683616bb
install default_handler for SIGINT initially as well;

diff -r 2b284ef75049 -r b24210573eca 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;