diff options
| author | Jim Fehrle | 2020-09-12 20:54:22 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-11-10 10:21:18 -0800 |
| commit | da9fd81c887024e991467d4dd586661c4ca01022 (patch) | |
| tree | 001e9bff33c8d759a8cb79351e2ef36a9839e0c8 /Makefile.doc | |
| parent | 7d8389d012aa8dbdeb7b82217087f1b7dfb2b24e (diff) | |
Convert logic.rst to prodn
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) |