aboutsummaryrefslogtreecommitdiff
path: root/bin/args.mli
diff options
context:
space:
mode:
authorChimrod <>2023-11-04 11:54:08 +0100
committerChimrod <>2023-11-04 11:54:08 +0100
commit673da2554d3e667e0a62d5c7bbf30999f1295dc1 (patch)
tree6fe7b79a4d70d31c6c405f6a943196a1b857dfdd /bin/args.mli
parent0f24d6d6c6a61c9a3f090649003df7daabff4d65 (diff)
List all the available tests on command line
Diffstat (limited to 'bin/args.mli')
-rw-r--r--bin/args.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/bin/args.mli b/bin/args.mli
index 5231cae..cffd0d0 100644
--- a/bin/args.mli
+++ b/bin/args.mli
@@ -3,4 +3,4 @@ type filters = { level : Qsp_syntax.Report.level option }
type t = { reset_line : bool; filters : filters }
(** All the arguments given from the command line *)
-val parse : unit -> string list * t
+val parse : list_tests:(Format.formatter -> unit) -> string list * t