diff options
| author | Emilio Jesus Gallego Arias | 2020-02-12 23:12:26 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-13 22:11:05 +0100 |
| commit | 8d73861eeae56321a106f28d07b47d5d6699939d (patch) | |
| tree | 31e8ee4a328798a9269141dab30c77e70b78bdfd /tools/dune | |
| parent | 4ea2825a4589b0c77225dd6f4caf98b12ac6dd6f (diff) | |
[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.
Diffstat (limited to 'tools/dune')
| -rw-r--r-- | tools/dune | 10 |
1 files changed, 9 insertions, 1 deletions
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) |