Merge PR #12994: Fix docgram's dune file following #12085.

Reviewed-by: ejgallego
coq · Sep 9, 2020 · cdfe69d · cdfe69d
2 parents 3d22134 + 461e0d6
commit cdfe69d
Showing 1 changed file with 2 additions and 1 deletion.
diff --git 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)