Re: [PG-devel] A few major bugs about exiting ProofGeneral with current CVS version

2011-09-12 Thread Hendrik Tews
Pierre Courtieu pierre.court...@cnam.fr writes: 2011/9/10 Erik Martin-Dorel erik.martin-do...@ens-lyon.fr: 3. Finally, it seems the function `proof-shell-exit' raises systematically an unexpected error. To reproduce it, run the (Coq) prover, then try: [M-: (setq

Re: [PG-devel] A few major bugs about exiting ProofGeneral with current CVS version

2011-09-11 Thread Tom Prince
On Sun, 11 Sep 2011 14:59:14 +0200, Pierre Courtieu pierre.court...@cnam.fr wrote: 2011/9/10 Erik Martin-Dorel erik.martin-do...@ens-lyon.fr: 1. Now the behavior of [C-x C-c] is not really consistent with the one of [C-c C-x]. Indeed, the second command calls yes-or-no-p before killing the