Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit 909feaea authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix trywhy3 incorrectly marking split tasks as valid.

Status of the parent task was updated before the new subtasks had been
associated to it. As a consequence, it was believed to be valid since it
had no children yet.
parent 14c07c17
......@@ -199,11 +199,7 @@ module Task =
let set_status id st =
let rec loop id st acc =
match
try
Some (get_info id)
with Not_found -> None
with
match get_info_opt id with
| Some info when info.status <> st ->
info.status <- st;
let acc = (UpdateStatus (st, id)) :: acc in
......@@ -269,10 +265,8 @@ let why3_split id =
[], _ -> ()
| [ child ], `Task(orig) when Why3.Task.task_equal child orig -> ()
| subtasks, _ ->
t.subtasks <- List.fold_left (fun acc t ->
let tid = register_task id t in
why3_prove tid;
tid :: acc) [] subtasks
t.subtasks <- List.map (fun t -> register_task id t) subtasks;
List.iter why3_prove t.subtasks
end
| _ -> ()
......
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