From 8d73861eeae56321a106f28d07b47d5d6699939d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 12 Feb 2020 23:12:26 +0100
Subject: [coqdep] Remove support for `-c` ocamldep replacement.

There is not need for coqdep to ship an `ocamldep` replacement, in
particular:

- not used in the main build since a long time
- not tested
- not kept up to date with upstream

This allows for a significant reduction of `coqdep` code, including
some duplicated code from `ocamllibdep`.

`coq_makefile` now uses `ocamllibdep` to process `mllib/mlpack` files,
so it has then to be installed.

We also remove the residual `-slash` option.
---
 tools/dune | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

(limited to 'tools/dune')

diff --git a/tools/dune b/tools/dune
index 204bd09535..c0e4e20f72 100644
--- a/tools/dune
+++ b/tools/dune
@@ -29,7 +29,15 @@
  (modules coqdep_lexer coqdep_common coqdep)
  (libraries coq.lib))
 
-(ocamllex coqdep_lexer)
+; Bare-bones mllib/mlpack parser
+(executable
+ (name ocamllibdep)
+ (public_name ocamllibdep)
+ (modules ocamllibdep)
+ (package coq)
+ (libraries unix))
+
+(ocamllex coqdep_lexer ocamllibdep)
 
 (executable
  (name coqwc)
-- 
cgit v1.2.3