equal
deleted
inserted
replaced
33 @if [ -d $${ISABELLEBIN:?}/Pure ];\ |
33 @if [ -d $${ISABELLEBIN:?}/Pure ];\ |
34 then echo Bad value for ISABELLEBIN: \ |
34 then echo Bad value for ISABELLEBIN: \ |
35 $(BIN) is the Isabelle source directory; \ |
35 $(BIN) is the Isabelle source directory; \ |
36 exit 1; \ |
36 exit 1; \ |
37 fi |
37 fi |
38 @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \ |
38 @case `basename "$(COMP)"` in \ |
39 poly*) echo 'make_database"$(BIN)/FOL"; quit();' \ |
39 poly*) echo 'make_database"$(BIN)/FOL"; quit();' \ |
40 | $(COMP) $(BIN)/Pure;\ |
40 | $(COMP) $(BIN)/Pure;\ |
41 if [ "$${MAKE_HTML}" = "true" ]; \ |
41 if [ "$${MAKE_HTML}" = "true" ]; \ |
42 then echo 'open PolyML; make_html := true; exit_use_dir".";' \ |
42 then echo 'open PolyML; make_html := true; exit_use_dir".";' \ |
43 | $(COMP) $(BIN)/FOL;\ |
43 | $(COMP) $(BIN)/FOL;\ |
61 |
61 |
62 $(BIN)/Pure: |
62 $(BIN)/Pure: |
63 cd ../Pure; $(MAKE) |
63 cd ../Pure; $(MAKE) |
64 |
64 |
65 test: ex/ROOT.ML $(BIN)/FOL $(EX_FILES) |
65 test: ex/ROOT.ML $(BIN)/FOL $(EX_FILES) |
66 @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \ |
66 @case `basename "$(COMP)"` in \ |
67 poly*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
67 poly*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
68 then echo 'make_html := true; exit_use_dir"ex"; quit();' \ |
68 then echo 'make_html := true; exit_use_dir"ex"; quit();' \ |
69 | $(COMP) $(BIN)/FOL;\ |
69 | $(COMP) $(BIN)/FOL;\ |
70 else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOL;\ |
70 else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOL;\ |
71 fi;;\ |
71 fi;;\ |