From 511134687d89fa5a5a5bbf45f40fa8ed615097d3 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sun, 29 Mar 2020 10:50:51 -0700
Subject: Add -no-update command line option to doc_grammar for Dune Fix
 makefile glitches

---
 Makefile.doc | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'Makefile.doc')

diff --git a/Makefile.doc b/Makefile.doc
index a8703b0acf..9da175f0e5 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -246,16 +246,16 @@ $(DOC_GRAM): $(DOC_GRAMCMO) coqpp/coqpp_parser.mli coqpp/coqpp_parser.ml doc/too
 # user-contrib/*/*.mlg omitted for now (e.g. ltac2)
 PLUGIN_MLGS := $(wildcard plugins/*/*.mlg)
 OMITTED_PLUGIN_MLGS := plugins/ssr/ssrparser.mlg plugins/ssr/ssrvernac.mlg plugins/ssrmatching/g_ssrmatching.mlg
-DOC_MLGS := */*.mlg $(sort $(filter-out $(OMITTED_PLUGIN_MLGS), $(PLUGIN_MLGS)))
-DOC_EDIT_MLGS := doc/tools/docgram/*.edit_mlg
-DOC_RSTS := doc/sphinx/*/*.rst
+DOC_MLGS := $(wildcard */*.mlg) $(sort $(filter-out $(OMITTED_PLUGIN_MLGS), $(PLUGIN_MLGS)))
+DOC_EDIT_MLGS := $(wildcard doc/tools/docgram/*.edit_mlg)
+DOC_RSTS := $(wildcard doc/sphinx/*/*.rst)
 
 doc/tools/docgram/fullGrammar: $(DOC_GRAM) $(DOC_MLGS)
 	$(SHOW)'DOC_GRAM'
 	$(HIDE)$(DOC_GRAM) -short -no-warn $(DOC_MLGS)
 
 #todo: add a dependency of sphinx on updated_rsts when we're ready
-doc/tools/docgram/orderedGrammar doc/tools/docgram/updated_rsts: $(DOC_GRAM) $(DOC_EDIT_MLGS)
+doc/tools/docgram/orderedGrammar doc/tools/docgram/updated_rsts: doc/tools/docgram/fullGrammar $(DOC_GRAM) $(DOC_EDIT_MLGS)
 	$(SHOW)'DOC_GRAM_RSTS'
 	$(HIDE)$(DOC_GRAM) -check-cmds $(DOC_MLGS) $(DOC_RSTS)
 
-- 
cgit v1.2.3