diff options
| author | Emilio Jesus Gallego Arias | 2020-01-17 01:25:06 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-01-17 18:02:33 +0100 |
| commit | a47e2f6587e3507a12d4d86b9769b93e01023350 (patch) | |
| tree | 495c3402489dfcfeb78d903a0e5011cf75017b37 /doc/stdlib/dune | |
| parent | 55ded80878d47037e49ca9b60f89c422d184899f (diff) | |
[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.
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 |