Thanks for the discussion on this:
> If nobody objects, I'll adopt solution 1 (see #421 for solution 2):
> Inside proof-shell-kill-function set a global variable
> proof-shell-exit-in-progress. When
> coq-switch-buffer-kill-proof-shell sees this it refrains from
> calling proof-shell-exit recursively.
I followed up on Trac. I guess solution 2 would be better, but I don't
object if you prefer to implement solution 1.
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
ProofGeneral-devel mailing list