Merge PR #11855: Build and install refman with Dune.

Ack-by: SkySkimmer
Reviewed-by: ejgallego

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))