aboutsummaryrefslogtreecommitdiff
path: root/doc/stdlib
diff options
context:
space:
mode:
Diffstat (limited to 'doc/stdlib')
-rw-r--r--doc/stdlib/dune14
1 files changed, 11 insertions, 3 deletions
diff --git a/doc/stdlib/dune b/doc/stdlib/dune
index 093c7a62b2..0b6ca5f178 100644
--- a/doc/stdlib/dune
+++ b/doc/stdlib/dune
@@ -13,6 +13,8 @@
(rule
(targets html)
+ (alias stdlib-html)
+ (package coq-doc)
(deps
; This will be replaced soon by `theories/**/*.v` soon, thanks to rgrinberg
(source_tree %{project_root}/theories)
@@ -31,6 +33,12 @@
(progn (cat %{header}) (cat index-list.html) (cat %{footer})))
(run cp _index.html html/index.html))))
-(alias
- (name stdlib-html)
- (deps html))
+; Installable directories are not yet fully supported by Dune. See
+; ocaml/dune#1868. Yet, this makes coq-doc.install a valid target to
+; generate the whole Coq documentation. And the result under
+; _build/install/default/doc/coq-doc looks just right!
+
+(install
+ (files (html as html/stdlib))
+ (section doc)
+ (package coq-doc))