diff options
| author | Théo Zimmermann | 2020-11-13 09:20:21 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-11-13 09:20:21 +0100 |
| commit | 53aa272821c2cd94e4b05382fa33449e851c7a90 (patch) | |
| tree | e7e52529768d9d85a1d99c89517a6b9fad390387 /doc/tools | |
| parent | 51e759fb2ff92dd89ab4823ddea3ea81be7f8046 (diff) | |
Fix dune rules for @check-gram following recent changes.
Diffstat (limited to 'doc/tools')
| -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 |