# HG changeset patch
# User bulwahn
# Date 1343110335 -7200
# Node ID aff95a0212d8e33c02b4147c3fc1cf28757fd127
# Parent  808a5ba619919c454986b639bf7f13b3e4c6e673
moving Quickcheck_Examples back to test to run a minimal test even with the mira testing infrastructure

diff -r 808a5ba61991 -r aff95a0212d8 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