moving Quickcheck_Examples back to test to run a minimal test even with the mira testing infrastructure
authorbulwahn
Tue, 24 Jul 2012 08:12:15 +0200
changeset 48489 aff95a0212d8
parent 48454 808a5ba61991
child 48490 1959baa22632
moving Quickcheck_Examples back to test to run a minimal test even with the mira testing infrastructure
src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Jul 23 19:07:01 2012 +0200
+++ b/src/HOL/IsaMakefile	Tue Jul 24 08:12:15 2012 +0200
@@ -59,6 +59,7 @@
   HOL-Nitpick_Examples \
   HOL-Number_Theory \
   HOL-Old_Number_Theory \
+  HOL-Quickcheck_Examples \
   HOL-Quotient_Examples \
   HOL-Predicate_Compile_Examples \
   HOL-Prolog \
@@ -93,7 +94,7 @@
   HOL-Nominal-Examples
 
 all: test-no-smlnj test images-no-smlnj images
-full: all benchmark HOL-Quickcheck_Examples
+full: all benchmark
 smlnj: test images