# HG changeset patch
# User wenzelm
# Date 971344037 -7200
# Node ID f6dfed43561d9c656445d6d3db239941ca4ca216
# Parent  1d6ae1ef8e6460fe01ed02a74255663adbd4ebe8
improved exhibit_interrupt;

diff -r 1d6ae1ef8e64 -r f6dfed43561d src/Pure/ML-Systems/polyml-4.0.ML
--- 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;