From 3b9cb50757b17565a042c25ee781c51bd529272d Mon Sep 17 00:00:00 2001 From: rikosellic <64517311+rikosellic@users.noreply.github.com> Date: Tue, 18 Aug 2026 16:58:25 +0800 Subject: [PATCH] chore: remove `verus-root` marker file --- src/verus.rs | 8 -------- 1 file changed, 8 deletions(-) diff --git a/src/verus.rs b/src/verus.rs index e9fcdcd..b979b7d 100644 --- a/src/verus.rs +++ b/src/verus.rs @@ -1405,14 +1405,6 @@ pub mod install { } } - let profile = if release { "release" } else { "debug" }; - File::create( - source_dir - .join("target-verus") - .join(profile) - .join("verus-root"), - )?; - status!("Verus build complete"); Ok(()) }