diff -r 647d557e9a40 -r 23564e91463e src/Cube/ex/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Cube/ex/ROOT.ML	Thu Mar 20 10:47:29 1997 +0100
@@ -0,0 +1,10 @@
+
+writeln"Root file for Cube examples";
+Cube_build_completed;    (*Cause examples to fail if Cube did*)
+
+proof_timing := true;
+
+use"ex.ML";
+
+cd "..";
+maketest"END: file for Lambda-Cube examples";