From 7848e1af92178b9cda99a07af63f41993200a497 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 17 Sep 2019 10:48:22 +0200
Subject: [PATCH] [server/batch] do not save options
---
src/plugins/server/server_batch.ml | 7 ++++---
1 file changed, 4 insertions(+), 3 deletions(-)
diff --git a/src/plugins/server/server_batch.ml b/src/plugins/server/server_batch.ml
index a180eaa9824..fa251825afa 100644
--- a/src/plugins/server/server_batch.ml
+++ b/src/plugins/server/server_batch.ml
@@ -42,6 +42,7 @@ module Batch = Senv.String_list
end)
let () = Parameter_customize.set_group batch_group
+let () = Parameter_customize.do_not_save ()
module BatchOutputDir = Senv.Empty_string
(struct
let option_name = "-server-batch-output-dir"
@@ -96,6 +97,8 @@ let rec execute_batch js =
let execute () =
begin
+ let files = Batch.get () in
+ Batch.clear () ; (* clear in any case *)
List.iter
begin fun file ->
Senv.feedback "Script %S" file ;
@@ -109,9 +112,7 @@ let execute () =
let out = open_out output in
Js.pretty_to_channel out response ;
close_out out
- end
- (Batch.get()) ;
- Batch.clear ()
+ end files
end
(* -------------------------------------------------------------------------- *)
--
GitLab