do not try to delete verus-root if it does not exist

verus-lang · Jan 9, 2025 · 1496213 · 1496213
1 parent a7c1e00
commit 1496213
Showing 1 changed file with 6 additions and 4 deletions.
diff --git 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()