changeset 4446 | 097004a470fb |
parent 2817 | 23564e91463e |
child 4583 | 6d9be46ea566 |
4445:de74b549f976 | 4446:097004a470fb |
---|---|
1 |
1 |
2 writeln"Root file for Cube examples"; |
2 writeln"Root file for Cube examples"; |
3 Cube_build_completed; (*Cause examples to fail if Cube did*) |
3 Cube_build_completed; (*Cause examples to fail if Cube did*) |
4 |
4 |
5 proof_timing := true; |
5 set proof_timing; |
6 |
6 |
7 use"ex.ML"; |
7 use "ex.ML"; |
8 |
|
9 cd ".."; |
|
10 maketest"END: file for Lambda-Cube examples"; |