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 ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
