diff --git a/ptests/ptests.ml b/ptests/ptests.ml index 259054fa280b6a06e6e51d1fbfd58f59e93d6786..05cb9f5a57aecfc8eeaa3d4d2c3bc4ffb8a6338e 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 });