author | wenzelm |
Thu, 29 Nov 2007 17:38:41 +0100 | |
changeset 25503 | fe14c6857f1d |
parent 25502 | 9200b36280c0 |
child 25504 | dc960d760052 |
--- 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 *)