diff options
| author | Emilio Jesus Gallego Arias | 2018-10-20 16:01:49 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-20 16:01:49 +0200 |
| commit | 32c1fc1ec2973a5b579f3e1f1ce6acf66488f24b (patch) | |
| tree | 8464436cea3cff29bd8dc00a0b238b3486c832e3 | |
| parent | 16e0223e111cdf1c61c421617dfda08de6e96720 (diff) | |
[dune] Remove rule for cLexer.ml4 -> cLexer.ml
When merging #8740 we didn't remove this rule.
The build didn't fails as Dune emits a warning for now [due to
compatibility with some schemes], but this will become an error in the
future.
| -rw-r--r-- | parsing/dune | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/parsing/dune b/parsing/dune index b70612a52b..f931321358 100644 --- a/parsing/dune +++ b/parsing/dune @@ -5,11 +5,6 @@ (libraries proofs)) (rule - (targets cLexer.ml) - (deps (:ml4-file cLexer.ml4)) - (action (run camlp5o -loc loc -impl %{ml4-file} -o %{targets}))) - -(rule (targets g_prim.ml) (deps (:mlg-file g_prim.mlg)) (action (run coqpp %{mlg-file}))) |