Commit 06f3a176 authored by François Bobot's avatar François Bobot

[Why3session] Fix prover specified uniquely

              when one of the field is empty.

              (Thx Jean-Christophe)
parent 8b32d86b
......@@ -94,7 +94,9 @@ let read_opt_prover s =
try
let l = Strings.rev_split ',' s in
match l with
| [altern;version;name] when List.for_all (fun s -> s.[0] <> '^') l ->
(** A prover specified uniquely *)
| [altern;version;name]
when List.for_all (fun s -> s = "" || s.[0] <> '^') l ->
Prover {Whyconf.prover_name = name;
prover_version = version;
prover_altern = altern}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment