diff options
| author | coqbot-app[bot] | 2020-11-15 15:25:39 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-15 15:25:39 +0000 |
| commit | 3ea3da24690e0e680c30b39e45f07a7e6500faac (patch) | |
| tree | ea772b55dc92d29a49ca576d9841fc54f2129dfe /doc | |
| parent | e476ded00efed5185a435f28551f1aa88b6c374a (diff) | |
| parent | 53aa272821c2cd94e4b05382fa33449e851c7a90 (diff) | |
Merge PR #13368: Fix dune rules for @check-gram following recent changes.
Reviewed-by: jfehrle
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/tools/docgram/dune | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune index 2a7b283f55..1c07d00d4f 100644 --- a/doc/tools/docgram/dune +++ b/doc/tools/docgram/dune @@ -12,7 +12,6 @@ (glob_files %{project_root}/parsing/*.mlg) (glob_files %{project_root}/toplevel/*.mlg) (glob_files %{project_root}/vernac/*.mlg) - ; All plugins except SSReflect for now (mimicking what is done in Makefile.doc) (glob_files %{project_root}/plugins/btauto/*.mlg) (glob_files %{project_root}/plugins/cc/*.mlg) (glob_files %{project_root}/plugins/derive/*.mlg) @@ -23,8 +22,11 @@ (glob_files %{project_root}/plugins/micromega/*.mlg) (glob_files %{project_root}/plugins/nsatz/*.mlg) (glob_files %{project_root}/plugins/omega/*.mlg) - (glob_files %{project_root}/plugins/rtauto/*.mlg) (glob_files %{project_root}/plugins/ring/*.mlg) + (glob_files %{project_root}/plugins/rtauto/*.mlg) + (glob_files %{project_root}/plugins/ssr/*.mlg) + (glob_files %{project_root}/plugins/ssrmatching/*.mlg) + (glob_files %{project_root}/plugins/ssrsearch/*.mlg) (glob_files %{project_root}/plugins/syntax/*.mlg) (glob_files %{project_root}/user-contrib/Ltac2/*.mlg) ; Sphinx files |