more information for the user how to deactivate quickcheck_narrowing if he does not want to use it
authorbulwahn
Wed, 20 Jul 2011 08:16:35 +0200
changeset 43911 a1da544e2652
parent 43910 575bf39e078b
child 43912 13e6a4e70219
more information for the user how to deactivate quickcheck_narrowing if he does not want to use it
src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Jul 20 08:16:33 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Jul 20 08:16:35 2011 +0200
@@ -458,7 +458,9 @@
   else
     (if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message
       ("Environment variable ISABELLE_GHC is not set. To use narrowing-based quickcheck, please set "
-        ^ "this variable to your GHC Haskell compiler in your settings file."); [Quickcheck.empty_result])
+        ^ "this variable to your GHC Haskell compiler in your settings file. "
+        ^ "To deactivate narrowing-based quickcheck, set quickcheck_narrowing_active to false.");
+      [Quickcheck.empty_result])
 
 (* setup *)