commit: non-critical, otherwise session restart will result in deadlock!
authorwenzelm
Thu, 29 Nov 2007 17:38:41 +0100
changeset 25503 fe14c6857f1d
parent 25502 9200b36280c0
child 25504 dc960d760052
commit: non-critical, otherwise session restart will result in deadlock!
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 *)