diff --git a/src/sail_lean_backend/sail_plugin_lean.ml b/src/sail_lean_backend/sail_plugin_lean.ml
index 4880dbcc0..007b999f5 100644
--- a/src/sail_lean_backend/sail_plugin_lean.ml
+++ b/src/sail_lean_backend/sail_plugin_lean.ml
@@ -71,6 +71,8 @@ open Interactive.State
 
 let opt_lean_output_dir : string option ref = ref None
 
+let opt_lean_force_output : bool ref = ref false
+
 let lean_version : string = "lean4:nightly-2024-09-25"
 
 let lean_options =
@@ -79,6 +81,10 @@ let lean_options =
       Arg.String (fun dir -> opt_lean_output_dir := Some dir),
       "<directory> set a custom directory to output generated Lean"
     );
+    ( "-lean_force_output",
+      Arg.Unit (fun () -> opt_lean_force_output := true),
+      " removes the content of the output directory if it is non-empty"
+    );
   ]
 
 (* TODO[javra]: Currently these are the same as the Coq rewrites, we might want to change them. *)
@@ -151,7 +157,11 @@ let create_lake_project (out_name : string) default_sail_dir =
   (* Change the base directory if the option '--lean-output-dir' is set *)
   let base_dir = match !opt_lean_output_dir with Some dir -> dir | None -> "." in
   let project_dir = Filename.concat base_dir out_name in
-  Unix.mkdir project_dir 0o775;
+  if !opt_lean_force_output && Sys.is_directory project_dir then (
+    let _ = Unix.system ("rm -r " ^ project_dir ^ "/*") in
+    ()
+  )
+  else Unix.mkdir project_dir 0o775;
   let gitignore = open_out (Filename.concat project_dir ".gitignore") in
   (* Ignore the `z3_problems` file generated by Sail and the `.lake` directory generated by lake*)
   output_string gitignore "/.lake";