1.1 --- a/src/Pure/Makefile Wed Mar 15 10:34:47 1995 +0100
1.2 +++ b/src/Pure/Makefile Wed Mar 15 10:53:58 1995 +0100
1.3 @@ -37,13 +37,13 @@
1.4 case "$(COMP)" in \
1.5 poly*) echo database=$${ML_DBASE:?'No Poly/ML database specified'};\
1.6 cp $(ML_DBASE) $(BIN)/Pure; chmod u+w $(BIN)/Pure;\
1.7 - echo 'PolyML.use"POLY";use"ROOT";' | $(COMP) $(BIN)/Pure;;\
1.8 + echo 'PolyML.use"POLY";use"ROOT" handle _=> exit 1;' | $(COMP) $(BIN)/Pure;;\
1.9 sml*) if [ ! '(' -d $${ISABELLEBIN:?} -a -w $${ISABELLEBIN:?} ')' ];\
1.10 then echo Bad value for ISABELLEBIN: \
1.11 $(BIN) is not a writable directory; \
1.12 exit 1; \
1.13 fi;\
1.14 - echo 'use"NJ.ML"; use"ROOT.ML"; xML"$(BIN)/Pure" banner;'\
1.15 + echo 'use"NJ.ML"; use"ROOT.ML" handle _=> exit 1; xML"$(BIN)/Pure" banner;'\
1.16 | $(COMP);;\
1.17 *) echo Bad value for ISABELLECOMP: \
1.18 $(COMP) is not poly or sml;;\