Hi Hendrik

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.  

Best wishes,

 - David

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

ProofGeneral-devel mailing list

Reply via email to