HOL,ZF/Makefile: enclosed multiple "use" calls in parentheses. This
ensures that if one dies, all die. BUT NOT Pure/Makefile, where
PolyML.use"POLY" makes the identifier "use" visible.
--- a/src/ZF/Makefile Thu Nov 10 11:06:44 1994 +0100
+++ b/src/ZF/Makefile Thu Nov 10 11:36:40 1994 +0100
@@ -70,9 +70,9 @@
#Load ex/ROOT.ML last since it creates the file "test"
test: $(BIN)/ZF $(IMP_FILES) $(EX_FILES)
case "$(COMP)" in \
- poly*) echo 'use"IMP/ROOT.ML"; use"ex/ROOT.ML"; quit();' | \
+ poly*) echo '(use"IMP/ROOT.ML"; use"ex/ROOT.ML"); quit();' | \
$(COMP) $(BIN)/ZF ;;\
- sml*) echo 'use"IMP/ROOT.ML"; use"ex/ROOT.ML";' | $(BIN)/ZF;;\
+ sml*) echo '(use"IMP/ROOT.ML"; use"ex/ROOT.ML");' | $(BIN)/ZF;;\
*) echo Bad value for ISABELLECOMP: \
$(COMP) is not poly or sml;;\
esac