aboutsummaryrefslogtreecommitdiff
path: root/tools/dune
diff options
context:
space:
mode:
authorGaëtan Gilbert2020-02-17 13:25:21 +0100
committerGaëtan Gilbert2020-02-17 13:25:21 +0100
commitcd7323ce0f7648f6db732292c0ded05c480be71f (patch)
treedc9056daf8854dec4342b361010035153c56949f /tools/dune
parentd122f7d5ffd5d3b26153a0ad7b74a669b8dd1c9d (diff)
parent8d73861eeae56321a106f28d07b47d5d6699939d (diff)
Merge PR #11589: [coqdep] Remove support for `-c` ocamldep replacement.
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
Diffstat (limited to 'tools/dune')
-rw-r--r--tools/dune10
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)