HOL/Makefile: now test depends upon SUBST_FILES
HOL/Makefile/SUBST_FILES: changed some filenames to upper case
HOL/Makefile: now executes ex/ROOT.ML after Subst/ROOT.ML
--- a/Makefile Fri Jul 15 14:04:28 1994 +0200
+++ b/Makefile Thu Jul 21 10:52:00 1994 +0200
@@ -37,8 +37,8 @@
SUBST_FILES = Subst/ROOT.ML Subst/AList.ML Subst/AList.thy\
Subst/Setplus.ML Subst/Setplus.thy\
- Subst/Subst.ML Subst/subst.thy\
- Subst/Unifier.ML Subst/unifier.thy\
+ Subst/Subst.ML Subst/Subst.thy\
+ Subst/Unifier.ML Subst/Unifier.thy\
Subst/UTerm.ML Subst/UTerm.thy\
Subst/UTLemmas.ML Subst/UTLemmas.thy
@@ -60,11 +60,13 @@
$(BIN)/Pure:
cd ../Pure; $(MAKE)
-test: ex/ROOT.ML $(BIN)/HOL $(EX_FILES)
+#Directory Subst also tests the system
+#Load ex/ROOT.ML last since it creates the file "test"
+test: $(BIN)/HOL $(SUBST_FILES) $(EX_FILES)
case "$(COMP)" in \
- poly*) echo 'use"ex/ROOT.ML"; use"Subst/ROOT.ML"; quit();' \
+ poly*) echo 'use"Subst/ROOT.ML"; use"ex/ROOT.ML"; quit();' \
| $(COMP) $(BIN)/HOL ;;\
- sml*) echo 'use"ex/ROOT.ML";use"Subst/ROOT.ML";' | $(BIN)/HOL;;\
+ sml*) echo 'use"Subst/ROOT.ML"; use"ex/ROOT.ML";' | $(BIN)/HOL;;\
*) echo Bad value for ISABELLECOMP: \
$(COMP) is not poly or sml;;\
esac