From ffce09acbe712cf447f5896ebdb98ba9d2d7faee Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 15 Jul 2019 15:38:58 +0200
Subject: [PATCH] [project] fix a rare but critical bug of Project.on leading
to an incorrect restoration of the former project
---
src/libraries/project/project.ml | 10 +++++-----
1 file changed, 5 insertions(+), 5 deletions(-)
diff --git a/src/libraries/project/project.ml b/src/libraries/project/project.ml
index f761614035b..27ff62f432d 100644
--- a/src/libraries/project/project.ml
+++ b/src/libraries/project/project.ml
@@ -379,12 +379,12 @@ let on ?selection p f x =
if old_current == p then f x
else
let set p = set_current ~on:true ?selection p in
- let set_to_old () =
+ let rec set_to_old old =
if not !keep_current then
try
(* if someone asks for keeping [p] as current during the execution of
[f], do not restore [old_current] at the end. *)
- set old_current
+ set old
with Invalid_argument _ ->
(* the old current project has been remove: replace it by the previous
one, if any *)
@@ -393,16 +393,16 @@ let on ?selection p f x =
old_current.unique_name
(current ()).unique_name
else
- Q.move_at_top (Q.nth 1 projects) projects
+ set_to_old (Q.nth 1 projects)
in
let go () =
set p;
let r = f x in
- set_to_old ();
+ set_to_old old_current;
r
in
if debug_atleast 1 then go ()
- else begin try go () with e -> set_to_old (); raise e end
+ else begin try go () with e -> set_to_old old_current; raise e end
(* [set_current] must never be called internally. *)
module Hide_set_current = struct let set_current () = assert false end
--
GitLab