# HG changeset patch # User blanchet # Date 1258478683 -3600 # Node ID 8bfe947305309d910713b30699dae35115b1c798 # Parent e441fede163d2c9a36ea4efbefe548fda1c7a282 run Nitpick examples if Kodkodi is available diff -r e441fede163d -r 8bfe94730530 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"];