Skip to content

Commit 7889f1f

Browse files
committed
Backport PR rocq-prover#15912: [coqide] Fix code to display goal in both top script and current script buffers
2 parents ab8cf4c + fc210ff commit 7889f1f

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

ide/coqide/coqide.ml

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -197,7 +197,9 @@ let create_session f =
197197
sn.coqops#set_forward_set_goals_of_dbg_session
198198
(fun msg ->
199199
sn.coqops#set_debug_goal msg;
200+
sn.last_db_goals <- msg;
200201
let osn = (find_secondary_sn sn) in
202+
osn.coqops#set_debug_goal msg;
201203
osn.last_db_goals <- msg);
202204
sn.coqops#set_forward_init_db (fun () -> !forward_init_db sn);
203205
let _ = set_drag sn.script#drag in

0 commit comments

Comments
 (0)