On Sun, 11 Sep 2011 14:59:14 +0200, Pierre Courtieu <[email protected]> wrote: > 2011/9/10 Erik Martin-Dorel <[email protected]>: > > 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). Tom _______________________________________________ ProofGeneral-devel mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
