From b46668fa43bb97f7d696978f687db3c97224ce4f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 2 Oct 2018 04:20:33 +0200
Subject: [dune] Install more files from `tools`.

These are needed for example for the test suite.
---
 tools/coqdoc/dune | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'tools/coqdoc')

diff --git a/tools/coqdoc/dune b/tools/coqdoc/dune
index 8e05c7d97e..b20d9f9b2e 100644
--- a/tools/coqdoc/dune
+++ b/tools/coqdoc/dune
@@ -1,3 +1,9 @@
+(install
+ (section lib)
+ (files
+  (coqdoc.css as tools/coqdoc/coqdoc.css)
+  (coqdoc.sty as tools/coqdoc/coqdoc.sty)))
+
 (executable
  (name main)
  (public_name coqdoc)
-- 
cgit v1.2.3