equal
deleted
inserted
replaced
27 SYNTAX_FILES = Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML\ |
27 SYNTAX_FILES = Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML\ |
28 Syntax/parser.ML Syntax/type_ext.ML Syntax/sextension.ML\ |
28 Syntax/parser.ML Syntax/type_ext.ML Syntax/sextension.ML\ |
29 Syntax/pretty.ML Syntax/printer.ML Syntax/syntax.ML\ |
29 Syntax/pretty.ML Syntax/printer.ML Syntax/syntax.ML\ |
30 Syntax/earley0A.ML Syntax/syn_ext.ML |
30 Syntax/earley0A.ML Syntax/syn_ext.ML |
31 |
31 |
32 THY_FILES = Thy/ROOT.ML Thy/scan.ML Thy/parse.ML Thy/syntax.ML Thy/read.ML |
32 THY_FILES = Thy/ROOT.ML Thy/scan.ML Thy/parse.ML Thy/thy_scan.ML Thy/thy_parse.ML Thy/thy_read.ML |
33 |
33 |
34 #Uses cp rather than make_database because Poly/ML allows only 3 levels |
34 #Uses cp rather than make_database because Poly/ML allows only 3 levels |
35 $(BIN)/Pure: $(FILES) $(SYNTAX_FILES) $(THY_FILES) $(ML_DBASE) |
35 $(BIN)/Pure: $(FILES) $(SYNTAX_FILES) $(THY_FILES) $(ML_DBASE) |
36 case "$(COMP)" in \ |
36 case "$(COMP)" in \ |
37 poly*) echo database=$${ML_DBASE:?'No Poly/ML database specified'};\ |
37 poly*) echo database=$${ML_DBASE:?'No Poly/ML database specified'};\ |