From 149621319cb415e0ebc2b3e8d927dc4ff6489513 Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Thu, 9 Jan 2025 19:23:28 +0100 Subject: [PATCH] do not try to delete verus-root if it does not exist --- tools/vargo/src/main.rs | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/tools/vargo/src/main.rs b/tools/vargo/src/main.rs index b0e36cebc..7a00322a1 100644 --- a/tools/vargo/src/main.rs +++ b/tools/vargo/src/main.rs @@ -1412,10 +1412,12 @@ cd "$( dirname "${{BASH_SOURCE[0]}}" )" !f.is_file() }) { - info(format!("removing {}", verus_root_path.display()).as_str()); - std::fs::remove_file(&verus_root_path).map_err(|x| { - format!("could not delete file {} ({x})", verus_root_path.display()) - })?; + if verus_root_path.exists() { + info(format!("removing {}", verus_root_path.display()).as_str()); + std::fs::remove_file(&verus_root_path).map_err(|x| { + format!("could not delete file {} ({x})", verus_root_path.display()) + })?; + } } else { std::mem::drop( std::fs::OpenOptions::new()