From d85f878e771888f098e458b2e37822b17b5de137 Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Thu, 18 Apr 2019 15:57:07 +0200
Subject: [PATCH] [cmdline] Fixed sequence of -remove-projects and -then
options
---
src/kernel_services/plugin_entry_points/kernel.ml | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 02f357e8ebb..6b53e263444 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -1522,7 +1522,9 @@ let _ =
let () =
Cmdline.run_after_configuring_stage
- (fun () -> Remove_projects.iter (fun project -> Project.remove ~project ()))
+ (fun () ->
+ Remove_projects.iter (fun project -> Project.remove ~project ());
+ Remove_projects.clear ())
(* ************************************************************************* *)
(** {2 Others options} *)
--
GitLab