equal
deleted
inserted
replaced
39 $(BIN)/Pure: $(FILES) $(SYNTAX_FILES) $(THY_FILES) $(ML_DBASE) |
39 $(BIN)/Pure: $(FILES) $(SYNTAX_FILES) $(THY_FILES) $(ML_DBASE) |
40 case "$(COMP)" in \ |
40 case "$(COMP)" in \ |
41 poly*) echo database=$${ML_DBASE:?'No Poly/ML database specified'};\ |
41 poly*) echo database=$${ML_DBASE:?'No Poly/ML database specified'};\ |
42 cp $(ML_DBASE) $(BIN)/Pure; chmod u+w $(BIN)/Pure;\ |
42 cp $(ML_DBASE) $(BIN)/Pure; chmod u+w $(BIN)/Pure;\ |
43 echo 'PolyML.use"POLY";use"ROOT" handle _=> exit 1;' \ |
43 echo 'PolyML.use"POLY";use"ROOT" handle _=> exit 1;' \ |
44 | $(COMP) $(BIN)/Pure;;\ |
44 | $(COMP) $(BIN)/Pure;\ |
|
45 discgarb -c $(BIN)/Pure;;\ |
45 sml*) if [ ! '(' -d $${ISABELLEBIN:?} -a -w $${ISABELLEBIN:?} ')' ];\ |
46 sml*) if [ ! '(' -d $${ISABELLEBIN:?} -a -w $${ISABELLEBIN:?} ')' ];\ |
46 then echo Bad value for ISABELLEBIN: \ |
47 then echo Bad value for ISABELLEBIN: \ |
47 $(BIN) is not a writable directory; \ |
48 $(BIN) is not a writable directory; \ |
48 exit 1; \ |
49 exit 1; \ |
49 fi;\ |
50 fi;\ |