diff options
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 30 |
1 files changed, 0 insertions, 30 deletions
diff --git a/Makefile.build b/Makefile.build index ff0e5dbaea..5b879220d0 100644 --- a/Makefile.build +++ b/Makefile.build @@ -363,36 +363,6 @@ $(COQPP): $(COQPPCMO) coqpp/coqpp_parser.mli coqpp/coqpp_parser.ml coqpp/coqpp_m $(SHOW)'OCAMLC -a $@' $(HIDE)$(OCAMLC) -I coqpp $^ -linkall -o $@ -DOC_GRAMCMO := $(addsuffix .cmo, $(addprefix coqpp/, coqpp_parse coqpp_lex)) - -$(DOC_GRAM): $(DOC_GRAMCMO) coqpp/coqpp_parser.mli coqpp/coqpp_parser.ml doc/tools/docgram/doc_grammar.ml - $(SHOW)'OCAMLC -a $@' - $(HIDE)$(OCAMLC) -I coqpp $^ -package str -linkall -linkpkg -o $@ - -DOC_MLGS := */*.mlg plugins/*/*.mlg -DOC_EDIT_MLGS := doc/tools/docgram/*_mlg -DOC_RSTS := doc/sphinx/*.rst 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 orderedGrammar and of *.rst on orderedGrammar when we're ready -doc/tools/docgram/orderedGrammar: $(DOC_GRAM) $(DOC_EDIT_MLGS) - $(SHOW)'DOC_GRAM_RSTS' - $(HIDE)$(DOC_GRAM) $(DOC_MLGS) $(DOC_RSTS) - -.PHONY: doc_gram doc_gram_rsts doc_gram_verify - -doc_gram: doc/tools/docgram/fullGrammar - -doc_gram_verify: doc/tools/docgram/fullGrammar - $(SHOW)'DOC_GRAM_VERIFY' - $(HIDE)$(DOC_GRAM) -short -no-warn -verify $(DOC_MLGS) $(DOC_RSTS) - -#todo: add dependency on $(DOC_RSTS) very soon -doc_gram_rsts: doc/tools/docgram/orderedGrammar - ########################################################################### # Specific rules for Uint63 ########################################################################### |