equal
deleted
inserted
replaced
32 | $(COMP) $(BIN)/LCF;\ |
32 | $(COMP) $(BIN)/LCF;\ |
33 elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
33 elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
34 then echo 'open PolyML; make_html := true; exit_use_dir"."; make_html := false;' | $(COMP) $(BIN)/LCF;\ |
34 then echo 'open PolyML; make_html := true; exit_use_dir"."; make_html := false;' | $(COMP) $(BIN)/LCF;\ |
35 else echo 'open PolyML; exit_use_dir".";' \ |
35 else echo 'open PolyML; exit_use_dir".";' \ |
36 | $(COMP) $(BIN)/LCF;\ |
36 | $(COMP) $(BIN)/LCF;\ |
37 fi;;\ |
37 fi;\ |
|
38 discgarb -c $(BIN)/LCF;;\ |
38 sml*) if [ "$${MAKE_HTML}" = "true" ]; \ |
39 sml*) if [ "$${MAKE_HTML}" = "true" ]; \ |
39 then echo 'make_html := true; exit_use_dir"."; xML"$(BIN)/LCF" banner;' | $(BIN)/FOL;\ |
40 then echo 'make_html := true; exit_use_dir"."; xML"$(BIN)/LCF" banner;' | $(BIN)/FOL;\ |
40 elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\ |
41 elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\ |
41 then echo 'make_html := true; exit_use_dir"."; make_html := false; xML"$(BIN)/LCF" banner;' \ |
42 then echo 'make_html := true; exit_use_dir"."; make_html := false; xML"$(BIN)/LCF" banner;' \ |
42 | $(BIN)/FOL;\ |
43 | $(BIN)/FOL;\ |