From 461e0d6b0e3b17224f23032c82d26fbb0dab4e74 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Tue, 8 Sep 2020 17:24:59 +0200 Subject: [PATCH] Fix docgram's dune file following #12085. --- doc/tools/docgram/dune | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune index a533a6d36736..ba07e6df0d97 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)