equal
deleted
inserted
replaced
45 | $(COMP) $(BIN)/HOL;\ |
45 | $(COMP) $(BIN)/HOL;\ |
46 else echo 'open PolyML; exit_use_dir".";' \ |
46 else echo 'open PolyML; exit_use_dir".";' \ |
47 | $(COMP) $(BIN)/HOL;\ |
47 | $(COMP) $(BIN)/HOL;\ |
48 fi;;\ |
48 fi;;\ |
49 sml*) if [ "$${MAKE_HTML-undefined}" != "undefined" ];\ |
49 sml*) if [ "$${MAKE_HTML-undefined}" != "undefined" ];\ |
50 then echo 'make_html (); exit_use_dir"."; xML"$(BIN)/HOL" banner;' | $(BIN)/Pure;\ |
50 then echo 'make_html := true; exit_use_dir"."; xML"$(BIN)/HOL" banner;' | $(BIN)/Pure;\ |
51 else echo 'exit_use_dir"."; xML"$(BIN)/HOL" banner;' \ |
51 else echo 'exit_use_dir"."; xML"$(BIN)/HOL" banner;' \ |
52 | $(BIN)/Pure;\ |
52 | $(BIN)/Pure;\ |
53 fi;;\ |
53 fi;;\ |
54 *) echo Bad value for ISABELLECOMP: \ |
54 *) echo Bad value for ISABELLECOMP: \ |
55 $(COMP) is not poly or sml; exit 1;;\ |
55 $(COMP) is not poly or sml; exit 1;;\ |