diff options
| author | Emilio Jesus Gallego Arias | 2018-10-19 13:37:54 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-19 13:37:54 +0200 |
| commit | 6ab9a8088394b710ae0b9f6d5711d2fe0509419f (patch) | |
| tree | 22be1a4cbcce1b4a29a9cbcfc3ef1249a11ca2e5 /Makefile.build | |
| parent | c3823156da73a63967d9d472e21560af1585b271 (diff) | |
| parent | 43afa49511033d7bbe5dec72e2e861930f8f9126 (diff) | |
Merge PR #8740: Removing the Camlp5 macros from CLexer.
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build index 4d19f9a2e1..77fcfc0abf 100644 --- a/Makefile.build +++ b/Makefile.build @@ -406,7 +406,7 @@ grammar/%.cmi: grammar/%.mli .PHONY: coqbinaries coqbyte -coqbinaries: $(TOPBINOPT) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE) +coqbinaries: $(TOPBINOPT) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE) $(GRAMMARCMA) coqbyte: $(TOPBYTE) $(CHICKENBYTE) # Special rule for coqtop, we imitate `ocamlopt` can delete the target |