diff options
| author | Théo Zimmermann | 2020-09-08 17:24:59 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-09-08 17:24:59 +0200 |
| commit | 461e0d6b0e3b17224f23032c82d26fbb0dab4e74 (patch) | |
| tree | f1c73dfde88832e25777713d3e72b39a922c8ccb /doc | |
| parent | 48f465dd5c5f9db416a7cd57b0acb86f17323ce3 (diff) | |
Fix docgram's dune file following #12085.
Diffstat (limited to 'doc')
| -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) |