From f9d2e46b1c72eebcde869269eec915ab8b92616a Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 29 Jan 2024 09:00:47 +0100
Subject: [PATCH] [wp] fix interactive prover startup

---
 src/plugins/wp/ProverWhy3.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index b97a388f6c9..62935c0fd4e 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1413,8 +1413,7 @@ let editor_command pconf =
 
 let scriptfile ~force ~ext wpo =
   let dir = Wp_parameters.get_session_dir ~force "interactive" in
-  let filenoext = Filepath.Normalized.concat dir wpo.Wpo.po_sid in
-  Filepath.Normalized.concat filenoext ext
+  Filepath.Normalized.concat dir (wpo.Wpo.po_sid ^ ext)
 
 let updatescript ~script driver task =
   let backup = Filepath.Normalized.concat script ".bak" in
-- 
GitLab