From c6a5b7bdce6e602adec2cfbbf8a32fd05e07942d Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Mon, 22 Mar 2021 08:31:18 +0100
Subject: [PATCH] [Ptests] Minor
---
ptests/ptests.ml | 9 ++++++---
1 file changed, 6 insertions(+), 3 deletions(-)
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index d3eaa58a945..1a09de07227 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -797,9 +797,12 @@ let config_options =
(fun _ s current ->
let new_top =
List.map
- (fun {toplevel; opts; logs; macros; timeout=_} ->
- { toplevel ; opts = make_custom_opts opts s; logs=logs @ current.dc_default_log;
- macros=current.dc_macros;timeout= current.dc_timeout})
+ (fun command ->
+ { command with opts= make_custom_opts command.opts s;
+ logs= command.logs @ current.dc_default_log;
+ macros = current.dc_macros;
+ timeout= current.dc_timeout
+ })
!default_parsing_env.current_default_cmds
in
{ current with dc_commands = new_top @ current.dc_commands;
--
GitLab