run Nitpick examples if Kodkodi is available
authorblanchet
Tue, 17 Nov 2009 18:24:43 +0100
changeset 33739 8bfe94730530
parent 33737 e441fede163d
child 33740 5fd36780760b
run Nitpick examples if Kodkodi is available
src/HOL/Nitpick_Examples/ROOT.ML
--- a/src/HOL/Nitpick_Examples/ROOT.ML	Tue Nov 17 14:10:31 2009 +0100
+++ b/src/HOL/Nitpick_Examples/ROOT.ML	Tue Nov 17 18:24:43 2009 +0100
@@ -5,4 +5,9 @@
 Nitpick examples.
 *)
 
-setmp_noncritical quick_and_dirty true (try use_thy) "Nitpick_Examples";
+Toplevel.debug := true;
+if getenv "KODKODI" = "" then
+  ()
+else
+  setmp_noncritical quick_and_dirty true use_thys
+                    ["Nitpick_Examples"];