From e4e98e11663a09d96605d44fd2d44f7403293d7e Mon Sep 17 00:00:00 2001 From: Marek Kubica Date: Fri, 13 Dec 2024 10:13:43 +0100 Subject: [PATCH] chore: Promote change due to #11172 (#11198) When building dune this change gets promoted when rebuilding. To prevent it leaking into unrelated PRs this PR adds it explicitely. Signed-off-by: Marek Kubica --- src/dune_rules/setup.defaults.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/dune_rules/setup.defaults.ml b/src/dune_rules/setup.defaults.ml index d96e454774b..4515addf7bc 100644 --- a/src/dune_rules/setup.defaults.ml +++ b/src/dune_rules/setup.defaults.ml @@ -11,7 +11,7 @@ let roots : string option Install.Roots.t = ; libexec_root = None } +let prefix : string option = None let toolchains = `Enabled let pkg_build_progress = `Disabled let lock_dev_tool = `Disabled -let prefix = None