equal
deleted
inserted
replaced
33 FILES = ROOT.ML Porder0.thy $(THYS) $(THYS:.thy=.ML) |
33 FILES = ROOT.ML Porder0.thy $(THYS) $(THYS:.thy=.ML) |
34 |
34 |
35 #Uses cp rather than make_database because Poly/ML allows only 3 levels |
35 #Uses cp rather than make_database because Poly/ML allows only 3 levels |
36 $(BIN)/HOLCF: $(BIN)/HOL $(FILES) |
36 $(BIN)/HOLCF: $(BIN)/HOL $(FILES) |
37 case "$(COMP)" in \ |
37 case "$(COMP)" in \ |
38 poly*) cp $(BIN)/HOL $(BIN)/HOLCF;\ |
38 poly*) cp $(BIN)/HOL $(BIN)/HOLCF; chmod u+w $(BIN)/HOLCF;\ |
39 if [ "$${MAKE_HTML}" = "true" ]; \ |
39 if [ "$${MAKE_HTML}" = "true" ]; \ |
40 then echo 'open PolyML; make_html := true; exit_use_dir".";' \ |
40 then echo 'open PolyML; make_html := true; exit_use_dir".";' \ |
41 | $(COMP) $(BIN)/HOLCF;\ |
41 | $(COMP) $(BIN)/HOLCF;\ |
42 elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
42 elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
43 then echo 'open PolyML; make_html := true; exit_use_dir"."; make_html := false;' | $(COMP) $(BIN)/HOLCF;\ |
43 then echo 'open PolyML; make_html := true; exit_use_dir"."; make_html := false;' | $(COMP) $(BIN)/HOLCF;\ |