From e1c0dae738c6b85950ad86344e4222f7f5bca1f6 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 27 Jan 2020 16:44:02 +0100
Subject: Don't install doc_grammar

Fix #11452
---
 Makefile.build | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile.build')

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
-- 
cgit v1.2.3