From e1359d9728d7d58785dd707db3ea06b3e33f004d Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Mon, 4 Jul 2022 16:32:16 +0200
Subject: [PATCH] [Ptests] 'STDOPT: options' defaults to 'STDOPT: +"options"'
---
ptests/ptests.ml | 7 ++-----
1 file changed, 2 insertions(+), 5 deletions(-)
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index 476d2ec14e6..237390a125c 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -765,7 +765,7 @@ end = struct
let make_custom_opts =
let space = Str.regexp " " in
- fun ~file ~dir stdopts s ->
+ fun ~file:_ ~dir:_ stdopts s ->
let rec aux opts s =
try
Scanf.sscanf s "%_[ ]%1[+#\\-]%_[ ]%S%_[ ]%s@\n"
@@ -777,10 +777,7 @@ end = struct
| _ -> assert false (* format of scanned string disallow it *))
with
| Scanf.Scan_failure _ ->
- if s <> "" then
- Format.eprintf "%a: unknown STDOPT configuration string: %s@."
- (SubDir.pp_file ~dir) file s;
- opts
+ if s <> "" then s::opts else opts
| End_of_file -> opts
in
(* NB: current settings does not allow to remove a multiple-argument
--
GitLab