# HG changeset patch
# User wenzelm
# Date 1014980145 -3600
# Node ID c2648d3e67a85c97243ef79dccc9bfdfbfbe9643
# Parent  1bfa0670f5924224e05ddb1b4be40dc50b9b585a
enable_interrupt is back!

diff -r 1bfa0670f592 -r c2648d3e67a8 src/Pure/ML-Systems/smlnj-0.93.ML
--- a/src/Pure/ML-Systems/smlnj-0.93.ML	Thu Feb 28 21:37:28 2002 +0100
+++ b/src/Pure/ML-Systems/smlnj-0.93.ML	Fri Mar 01 11:55:45 2002 +0100
@@ -125,6 +125,8 @@
       val _ = unchange ();
     in release result end;
 
+fun enable_interrupt f = change_mask interruptible unmask_signals mask_signals f;
+
 in
 
 fun ignore_interrupt f = change_mask (not o interruptible) mask_signals unmask_signals f;
@@ -142,7 +144,7 @@
     fun proceed cont =
       let
         val _ = set_handler cont;
-        val result = unmask_interrupt (capture f) x;
+        val result = enable_interrupt (capture f) x;
         val _ = reset_handler ();
       in release result end;
   in