equal
deleted
inserted
replaced
27 EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/If.ML ex/If.thy ex/int.ML\ |
27 EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/If.ML ex/If.thy ex/int.ML\ |
28 ex/intro.ML ex/Nat.ML ex/Nat.thy ex/Prolog.ML ex/Prolog.thy\ |
28 ex/intro.ML ex/Nat.ML ex/Nat.thy ex/Prolog.ML ex/Prolog.thy\ |
29 ex/prop.ML ex/quant.ML |
29 ex/prop.ML ex/quant.ML |
30 |
30 |
31 $(BIN)/FOLP: $(BIN)/Pure $(FILES) |
31 $(BIN)/FOLP: $(BIN)/Pure $(FILES) |
32 @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \ |
32 @case `basename "$(COMP)"` in \ |
33 poly*) echo 'make_database"$(BIN)/FOLP"; quit();' \ |
33 poly*) echo 'make_database"$(BIN)/FOLP"; quit();' \ |
34 | $(COMP) $(BIN)/Pure;\ |
34 | $(COMP) $(BIN)/Pure;\ |
35 if [ "$${MAKE_HTML}" = "true" ]; \ |
35 if [ "$${MAKE_HTML}" = "true" ]; \ |
36 then echo 'open PolyML; make_html := true; exit_use_dir".";' \ |
36 then echo 'open PolyML; make_html := true; exit_use_dir".";' \ |
37 | $(COMP) $(BIN)/FOLP;\ |
37 | $(COMP) $(BIN)/FOLP;\ |
55 |
55 |
56 $(BIN)/Pure: |
56 $(BIN)/Pure: |
57 cd ../Pure; $(MAKE) |
57 cd ../Pure; $(MAKE) |
58 |
58 |
59 test: ex/ROOT.ML $(BIN)/FOLP $(EX_FILES) |
59 test: ex/ROOT.ML $(BIN)/FOLP $(EX_FILES) |
60 @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \ |
60 @case `basename "$(COMP)"` in \ |
61 poly*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
61 poly*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
62 then echo 'make_html := true; exit_use_dir"ex"; quit();' \ |
62 then echo 'make_html := true; exit_use_dir"ex"; quit();' \ |
63 | $(COMP) $(BIN)/FOLP;\ |
63 | $(COMP) $(BIN)/FOLP;\ |
64 else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOLP;\ |
64 else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOLP;\ |
65 fi;;\ |
65 fi;;\ |