diff options
| author | Théo Zimmermann | 2020-01-17 19:37:58 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-01-17 19:37:58 +0100 |
| commit | 1f3ad4f8ebbf48d68488d19335d3c2db18e248f4 (patch) | |
| tree | 349f615d456252c593e4a0512de732c914fa9903 /doc/stdlib/dune | |
| parent | 58a9fa018995aa59e30bb7156a6c91b640f88730 (diff) | |
| parent | c3cf1451e6a07a30f58b5704474b19ce7feb1afa (diff) | |
Merge PR #11413: [doc] [ltac2] Build Ltac2 documentation
Reviewed-by: Zimmi48
Diffstat (limited to 'doc/stdlib/dune')
| -rw-r--r-- | doc/stdlib/dune | 6 |
1 files changed, 4 insertions, 2 deletions
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 |