Debugging code (error_depth) removed.
authorballarin
Thu, 10 Mar 2005 09:11:57 +0100
changeset 15597 b5f5722ed703
parent 15596 8665d08085df
child 15598 4ab52355bb53
Debugging code (error_depth) removed.
src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Mar 09 18:44:52 2005 +0100
+++ b/src/Pure/ROOT.ML	Thu Mar 10 09:11:57 2005 +0100
@@ -11,7 +11,6 @@
 
 
 print_depth 10;
-error_depth 30;
 
 (*fake hiding of private structures*)
 structure Hidden = struct end;