# HG changeset patch
# User blanchet
# Date 1258481282 -3600
# Node ID 83ae8b7e27689fd0b0ea0cb0cdd70452026d8996
# Parent  5fd36780760b955523add38da5eb8c832afd0e93
removed "debug := true" that shouldn't have been submitted in the first place

diff -r 5fd36780760b -r 83ae8b7e2768 src/HOL/Nitpick_Examples/ROOT.ML
--- a/src/HOL/Nitpick_Examples/ROOT.ML	Tue Nov 17 18:25:05 2009 +0100
+++ b/src/HOL/Nitpick_Examples/ROOT.ML	Tue Nov 17 19:08:02 2009 +0100
@@ -5,7 +5,6 @@
 Nitpick examples.
 *)
 
-Toplevel.debug := true;
 if getenv "KODKODI" = "" then
   ()
 else