From b008983c0a9efe35b5471d2e855f12420830e4c5 Mon Sep 17 00:00:00 2001 From: Andre Maroneze <andre.oliveiramaroneze@cea.fr> Date: Tue, 18 Dec 2018 18:40:31 +0100 Subject: [PATCH] [Ptests] fix LOG directive --- ptests/ptests.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/ptests/ptests.ml b/ptests/ptests.ml index 259054fa280..05cb9f5a57a 100644 --- a/ptests/ptests.ml +++ b/ptests/ptests.ml @@ -711,7 +711,8 @@ let config_options = !current_default_cmds in { current with dc_toplevels = new_top @ current.dc_toplevels; - dc_default_log = !current_default_log }); + dc_default_log = !current_default_log @ + current.dc_default_log }); "FILEREG", (fun _ s current -> { current with dc_test_regexp = s }); -- GitLab