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

coq · Sep 10, 2020 · 9f555ce · 9f555ce
2 parents 6895fe3 + d36d5b1
commit 9f555ce
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)