From 50ad504c077d46d4dce341e8b29d5ca6f20f9d42 Mon Sep 17 00:00:00 2001 From: Damien Doligez Date: Wed, 2 Feb 2022 12:54:09 +0100 Subject: [PATCH 1/2] bootstrap.ml: ignore errors when trying to remove generated files Signed-off-by: Damien Doligez --- bootstrap.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/bootstrap.ml b/bootstrap.ml index 3999b0e1ea4..157fdc5a893 100644 --- a/bootstrap.ml +++ b/bootstrap.ml @@ -45,7 +45,7 @@ let () = String.length fn >= String.length duneboot && String.sub fn ~pos:0 ~len:(String.length duneboot) = duneboot then - Sys.remove fn)) + try Sys.remove fn with Sys_error _ -> ())) let runf fmt = ksprintf From 514c627eb814b00823fa5ab7808649b5e88e46c4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicol=C3=A1s=20Ojeda=20B=C3=A4r?= Date: Thu, 3 Feb 2022 07:37:27 +0100 Subject: [PATCH 2/2] CHANGES.md MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Signed-off-by: Nicolás Ojeda Bär --- CHANGES.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index 839303f4219..0740a43bc15 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -305,6 +305,9 @@ Unreleased - Add link_flags in the env stanza (#5215) +- Bootstrap: ignore errors when trying to remove generated files. (#5407, + @damiendoligez) + 2.9.3 (unreleased) ------------------