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/dune | 21 +++++++++++++--------
 1 file changed, 13 insertions(+), 8 deletions(-)

(limited to 'tools/dune')

diff --git a/tools/dune b/tools/dune
index 05a620fb07..20048fde52 100644
--- a/tools/dune
+++ b/tools/dune
@@ -1,8 +1,11 @@
-(executable
- (name coqc)
- (public_name coqc)
- (modules coqc)
- (libraries coq.toplevel))
+(install
+ (section lib)
+ (files
+  (CoqMakefile.in as tools/CoqMakefile.in)
+  (TimeFileMaker.py as tools/TimeFileMaker.py)
+  (make-one-time-file.py as tools/make-one-time-file.py)
+  (make-both-time-files.py as tools/make-both-time-files.py)
+  (make-both-single-timing-files.py as tools/make-both-single-timing-files.py)))
 
 (executable
  (name coq_makefile)
@@ -10,9 +13,11 @@
  (modules coq_makefile)
  (libraries coq.lib))
 
-(install
- (section lib)
- (files (CoqMakefile.in as tools/CoqMakefile.in)))
+(executable
+ (name coqc)
+ (public_name coqc)
+ (modules coqc)
+ (libraries coq.toplevel))
 
 (executable
  (name coqdep)
-- 
cgit v1.2.3