# HG changeset patch
# User wenzelm
# Date 970144523 -7200
# Node ID 567b9676cb0a827d25d4f87cd616644a7e7770d7
# Parent  44da60e5331be748b49e4cd7633edb226c3436f8
only run quick_and_dirty version by default;

diff -r 44da60e5331b -r 567b9676cb0a Admin/Benchmarks/HOL-datatype/ROOT.ML
--- a/Admin/Benchmarks/HOL-datatype/ROOT.ML	Thu Sep 28 14:34:49 2000 +0200
+++ b/Admin/Benchmarks/HOL-datatype/ROOT.ML	Thu Sep 28 14:35:23 2000 +0200
@@ -11,6 +11,8 @@
 warning "\nset quick_and_dirty\n"; set quick_and_dirty;
 seq time_use_thy tests;
 
+(* not run by default
 warning "\nreset quick_and_dirty\n"; reset quick_and_dirty;
 seq remove_thy tests;
 seq time_use_thy tests;
+*)