From 80f3011eb5ca479b9b1f059c0f04e131028d5312 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 18 Mar 2020 16:07:19 +0100
Subject: Build and install refman with Dune.

---
 doc/stdlib/dune | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

(limited to 'doc/stdlib')

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))
-- 
cgit v1.2.3