On Sun, 11 Sep 2011 14:59:14 +0200, Pierre Courtieu <pierre.court...@cnam.fr> 
> 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
> > prover, while the first one now exits Emacs silently!
> Hello, I don't understand this remark. The keybinging [C-x C-c] has
> nothing to do with proofgeneral. It is the standard emacs keybinding
> to exit emacs silently. Why C-c C-x should be consistent with it?

I think the issue is that with just proof-general open in emacs, and no
unsaved files, (and process-query-on-exit flag off), then C-c C-x
prompts about killing the prover, but that C-x C-c just silently kills
it and emacs.

Before, (with process-querry-on-exit-flag on), they would both prompt
before killing things (C-c C-x twice).


ProofGeneral-devel mailing list

Reply via email to