src/Cube/ex/ROOT.ML
changeset 4446 097004a470fb
parent 2817 23564e91463e
child 4583 6d9be46ea566
--- a/src/Cube/ex/ROOT.ML	Fri Dec 19 10:17:04 1997 +0100
+++ b/src/Cube/ex/ROOT.ML	Fri Dec 19 10:18:03 1997 +0100
@@ -2,9 +2,6 @@
 writeln"Root file for Cube examples";
 Cube_build_completed;    (*Cause examples to fail if Cube did*)
 
-proof_timing := true;
+set proof_timing;
 
-use"ex.ML";
-
-cd "..";
-maketest"END: file for Lambda-Cube examples";
+use "ex.ML";