equal
deleted
inserted
replaced
41 | $(COMP) $(BIN)/CCL;\ |
41 | $(COMP) $(BIN)/CCL;\ |
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)/CCL;\ |
43 then echo 'open PolyML; make_html := true; exit_use_dir"."; make_html := false;' | $(COMP) $(BIN)/CCL;\ |
44 else echo 'open PolyML; exit_use_dir".";' \ |
44 else echo 'open PolyML; exit_use_dir".";' \ |
45 | $(COMP) $(BIN)/CCL;\ |
45 | $(COMP) $(BIN)/CCL;\ |
46 fi;;\ |
46 fi;\ |
|
47 discgarb -c $(BIN)/CCL;;\ |
47 sml*) if [ "$${MAKE_HTML}" = "true" ]; \ |
48 sml*) if [ "$${MAKE_HTML}" = "true" ]; \ |
48 then echo 'make_html := true; exit_use_dir"."; xML"$(BIN)/CCL" banner;' | $(BIN)/FOL;\ |
49 then echo 'make_html := true; exit_use_dir"."; xML"$(BIN)/CCL" banner;' | $(BIN)/FOL;\ |
49 elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\ |
50 elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\ |
50 then echo 'make_html := true; exit_use_dir"."; make_html := false; xML"$(BIN)/CCL" banner;' \ |
51 then echo 'make_html := true; exit_use_dir"."; make_html := false; xML"$(BIN)/CCL" banner;' \ |
51 | $(BIN)/FOL;\ |
52 | $(BIN)/FOL;\ |