From a47e2f6587e3507a12d4d86b9769b93e01023350 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 17 Jan 2020 01:25:06 +0100
Subject: [doc] [dune] [ltac2] Build Ltac2 documentation [dune build system]

This partially fixes #10139 ; we now build the Ltac2 documentation and
deploy it.

The fix here can be used for inspiration to do the make-based part.
---
 doc/stdlib/dune | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'doc/stdlib/dune')

diff --git a/doc/stdlib/dune b/doc/stdlib/dune
index 7fe2493fbf..828caecabc 100644
--- a/doc/stdlib/dune
+++ b/doc/stdlib/dune
@@ -5,7 +5,8 @@
  (deps
    make-library-index index-list.html.template hidden-files
    (source_tree %{project_root}/theories)
-   (source_tree %{project_root}/plugins))
+   (source_tree %{project_root}/plugins)
+   (source_tree %{project_root}/user-contrib))
  (action
   (chdir %{project_root}
    ; On windows run will fail
@@ -17,6 +18,7 @@
    ; This will be replaced soon by `theories/**/*.v` soon, thanks to rgrinberg
    (source_tree %{project_root}/theories)
    (source_tree %{project_root}/plugins)
+   (source_tree %{project_root}/user-contrib)
    (:header %{project_root}/doc/common/styles/html/coqremote/header.html)
    (:footer %{project_root}/doc/common/styles/html/coqremote/footer.html)
    ; For .glob files, should be gone when Coq Dune is smarter.
@@ -24,7 +26,7 @@
  (action
   (progn
    (run mkdir -p html)
-   (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -R %{project_root}/plugins Coq $(find %{project_root}/theories %{project_root}/plugins -name *.v)")
+   (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -R %{project_root}/plugins Coq -Q %{project_root}/user-contrib/Ltac2 Ltac2 $(find %{project_root}/theories %{project_root}/plugins %{project_root}/user-contrib -name *.v)")
    (run mv html/index.html html/genindex.html)
    (with-stdout-to
      _index.html
-- 
cgit v1.2.3