# HG changeset patch
# User wenzelm
# Date 1196354321 -3600
# Node ID fe14c6857f1dd4a64e65f446ab7353552cf7669a
# Parent  9200b36280c012a012c4b471282b88a899231fba
commit: non-critical, otherwise session restart will result in deadlock!

diff -r 9200b36280c0 -r fe14c6857f1d src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Thu Nov 29 17:08:26 2007 +0100
+++ b/src/Pure/General/secure.ML	Thu Nov 29 17:38:41 2007 +0100
@@ -52,7 +52,7 @@
   (secure_mltext (); orig_use_file Output.ml_output true name);
 
 (*commit is dynamically bound!*)
-fun commit () = CRITICAL (fn () => orig_use_text "" Output.ml_output false "commit();");
+fun commit () = orig_use_text "" Output.ml_output false "commit();";
 
 
 (* shell commands *)