# HG changeset patch
# User wenzelm
# Date 858853399 -3600
# Node ID 50bac845de6f106dcab0307f95f740fd5e9d53df
# Parent  b1dcacc4bc26e0254f766a7d41e48b690d10b552
exit_use_dir;

diff -r b1dcacc4bc26 -r 50bac845de6f src/CTT/Makefile
--- a/src/CTT/Makefile	Thu Mar 20 11:11:53 1997 +0100
+++ b/src/CTT/Makefile	Thu Mar 20 11:23:19 1997 +0100
@@ -61,8 +61,8 @@
 
 test:	ex/ROOT.ML $(BIN)/CTT  $(EX_FILES) 
 	@case `basename "$(COMP)"` in \
-	poly*)	echo 'exit_use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/CTT ;;\
-	sml*)	echo 'exit_use"ex/ROOT.ML";' | $(BIN)/CTT;;\
+	poly*)	echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/CTT ;;\
+	sml*)	echo 'exit_use_dir"ex";' | $(BIN)/CTT;;\
 	*)	echo Bad value for ISABELLECOMP: \
 			\"$(COMP)\" is not poly or sml;;\
 	esac
diff -r b1dcacc4bc26 -r 50bac845de6f src/CTT/ex/ROOT.ML
--- a/src/CTT/ex/ROOT.ML	Thu Mar 20 11:11:53 1997 +0100
+++ b/src/CTT/ex/ROOT.ML	Thu Mar 20 11:23:19 1997 +0100
@@ -6,15 +6,16 @@
 Executes all examples for Constructive Type Theory. 
 *)
 
-CTT_build_completed;    (*Cause examples to fail if CTT did*)
+writeln"Root file for CTT examples";
 
-writeln"Root file for CTT examples";
+CTT_build_completed;    (*Cause examples to fail if CTT did*)
 
 print_depth 2;  
 proof_timing := true;
-time_use "ex/typechk.ML";
-time_use "ex/elim.ML";
-time_use "ex/equal.ML";
-time_use "ex/synth.ML";
+time_use "typechk.ML";
+time_use "elim.ML";
+time_use "equal.ML";
+time_use "synth.ML";
 
+cd "..";
 maketest"END: Root file for CTT examples";