diff options
| author | coqbot-app[bot] | 2020-09-09 13:27:19 +0000 |
|---|---|---|
| committer | GitHub | 2020-09-09 13:27:19 +0000 |
| commit | cdfe69d6da6b32338ba74c9f599c74389089c9dd (patch) | |
| tree | 24ece09343fd37b1a8d2fe19826e17c280871600 | |
| parent | 3d22134121ddeeb2052266d5f2cbcc097a5f0388 (diff) | |
| parent | 461e0d6b0e3b17224f23032c82d26fbb0dab4e74 (diff) | |
Merge PR #12994: Fix docgram's dune file following #12085.
Reviewed-by: ejgallego
| -rw-r--r-- | doc/tools/docgram/dune | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune index a533a6d367..ba07e6df0d 100644 --- a/doc/tools/docgram/dune +++ b/doc/tools/docgram/dune @@ -12,7 +12,7 @@ (glob_files %{project_root}/parsing/*.mlg) (glob_files %{project_root}/toplevel/*.mlg) (glob_files %{project_root}/vernac/*.mlg) - ; All plugins except SSReflect and Ltac2 for now (mimicking what is done in Makefile.doc) + ; 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) @@ -26,6 +26,7 @@ (glob_files %{project_root}/plugins/rtauto/*.mlg) (glob_files %{project_root}/plugins/setoid_ring/*.mlg) (glob_files %{project_root}/plugins/syntax/*.mlg) + (glob_files %{project_root}/user-contrib/Ltac2/*.mlg) ; Sphinx files (glob_files %{project_root}/doc/sphinx/language/*.rst) (glob_files %{project_root}/doc/sphinx/proof-engine/*.rst) |