equal
deleted
inserted
replaced
17 #if it is out of date, since this Makefile does not know its dependencies! |
17 #if it is out of date, since this Makefile does not know its dependencies! |
18 |
18 |
19 BIN = $(ISABELLEBIN) |
19 BIN = $(ISABELLEBIN) |
20 COMP = $(ISABELLECOMP) |
20 COMP = $(ISABELLECOMP) |
21 FILES = ROOT.ML lk.thy lk.ML |
21 FILES = ROOT.ML lk.thy lk.ML |
|
22 EX_FILES = ex/ROOT.ML ex/hardquant.ML ex/prop.ML ex/quant.ML |
22 |
23 |
23 $(BIN)/LK: $(BIN)/Pure $(FILES) |
24 $(BIN)/LK: $(BIN)/Pure $(FILES) |
24 case "$(COMP)" in \ |
25 case "$(COMP)" in \ |
25 poly*) echo 'make_database"$(BIN)/LK"; quit();' \ |
26 poly*) echo 'make_database"$(BIN)/LK"; quit();' \ |
26 | $(COMP) $(BIN)/Pure;\ |
27 | $(COMP) $(BIN)/Pure;\ |
30 esac |
31 esac |
31 |
32 |
32 $(BIN)/Pure: |
33 $(BIN)/Pure: |
33 cd ../Pure; $(MAKE) |
34 cd ../Pure; $(MAKE) |
34 |
35 |
35 test: ex/ROOT.ML $(BIN)/LK |
36 test: ex/ROOT.ML $(BIN)/LK $(EX_FILES) |
36 case "$(COMP)" in \ |
37 case "$(COMP)" in \ |
37 poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/LK ;;\ |
38 poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/LK ;;\ |
38 sml*) echo 'use"ex/ROOT.ML";' | $(BIN)/LK;;\ |
39 sml*) echo 'use"ex/ROOT.ML";' | $(BIN)/LK;;\ |
39 *) echo Bad value for ISABELLECOMP;;\ |
40 *) echo Bad value for ISABELLECOMP;;\ |
40 esac |
41 esac |