diff options
Diffstat (limited to 'utils')
-rw-r--r-- | utils/dune | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/utils/dune b/utils/dune index a9f7629803..ec264d3405 100644 --- a/utils/dune +++ b/utils/dune @@ -15,12 +15,10 @@ (rule (targets config.ml) (mode fallback) - (deps (:mk Makefile) - ../Makefile.config - ; for now the utils Makefile does not use build_config - config.mlp - config.common.ml) - (action (system "make -f %{mk} %{targets}"))) + (deps config.generated.ml config.common.ml) + (action + (with-stdout-to %{targets} + (system "cat %{deps}")))) (rule (targets domainstate.ml) |