diff options
| author | coqbot-app[bot] | 2020-11-10 21:30:52 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-10 21:30:52 +0000 |
| commit | 417e8c513e4372bcd622603912cfb2d9f1069619 (patch) | |
| tree | c999417af80830af45f685751337bf3124652b92 /Makefile.doc | |
| parent | fa6c67d721d4178d6b82571feef33c887aef5ba2 (diff) | |
| parent | da9fd81c887024e991467d4dd586661c4ca01022 (diff) | |
Merge PR #13315: Convert logic chapter to prodn
Reviewed-by: Zimmi48
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/Makefile.doc b/Makefile.doc index 473a70fb72..a5ff8e0123 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -248,8 +248,7 @@ $(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 \ - plugins/ssrsearch/g_search.mlg +OMITTED_PLUGIN_MLGS := DOC_MLGS := $(wildcard */*.mlg) $(sort $(filter-out $(OMITTED_PLUGIN_MLGS), $(PLUGIN_MLGS))) \ user-contrib/Ltac2/g_ltac2.mlg DOC_EDIT_MLGS := $(wildcard doc/tools/docgram/*.edit_mlg) |