# HG changeset patch
# User lcp
# Date 774780720 -7200
# Node ID 3f4976d8c97f38c8a11f05cde90125ac42b83370
# Parent  d94d0b324b4bc03ee13508b2f0050c07a175cfd5
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

diff -r d94d0b324b4b -r 3f4976d8c97f Makefile
--- 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