From a210c44e2f375d8aa7e18040ace3cb75248e830b Mon Sep 17 00:00:00 2001 From: Etienne Millon Date: Mon, 24 Jul 2023 17:20:38 +0200 Subject: [PATCH] fix: disable background digests on Windows Fixes #8228 In some cases when the shared cache is enabled, some temporary directories cannot be removed. Signed-off-by: Etienne Millon --- CHANGES.md | 4 ++++ src/dune_config/config.ml | 5 ++++- 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/CHANGES.md b/CHANGES.md index 94ee3264728..a35a623c376 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -24,6 +24,10 @@ Unreleased - Fix permission errors when `sendfile` is not available (#8234, fixes #8120, @emillon) +- Disable background digests on Windows. This prevents an issue where + unremovable files would make dune crash when the shared cache is enabled. + (#8243, fixes #8228, @emillon) + 3.9.1 (2023-07-06) ------------------ diff --git a/src/dune_config/config.ml b/src/dune_config/config.ml index eac22094920..b96e7dceaf3 100644 --- a/src/dune_config/config.ml +++ b/src/dune_config/config.ml @@ -116,7 +116,10 @@ let background_digests = let t = { name = "background_digests" ; of_string = Toggle.of_string - ; value = background_default + ; value = + (match Platform.OS.value with + | Linux -> `Enabled + | _ -> `Disabled) } in register t;