diff options
| author | Enrico Tassi | 2020-02-06 15:25:32 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2020-02-06 15:25:32 +0100 |
| commit | c6e89e2b13d7fa99aaaaf02fc3430ae6c5f00beb (patch) | |
| tree | c97ddb7d8f150f2f9214106029d8faa6631550b2 /Makefile.build | |
| parent | 746ff224e7fba9fc81b8a9499f9fec2ab8af4570 (diff) | |
| parent | e1c0dae738c6b85950ad86344e4222f7f5bca1f6 (diff) | |
Merge PR #11458: Don't install doc_grammar
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 a8ae040f8e..814305a2fe 100644 --- a/Makefile.build +++ b/Makefile.build @@ -417,7 +417,7 @@ $(COQTOPBYTE): $(COQTOP_BYTE) $(LINKCMO) $(LIBCOQRUN) ########################################################################### .PHONY: tools -tools: $(TOOLS) $(OCAMLLIBDEP) $(COQDEPBOOT) +tools: $(TOOLS) $(OCAMLLIBDEP) $(COQDEPBOOT) $(DOC_GRAM) # coqdep_boot : a basic version of coqdep, with almost no dependencies. # We state these dependencies here explicitly, since some .ml.d files |