branch: elpa/proof-general
commit 2d4d0317a6e6bea92c1bfd0148f3cf83e6692841
Merge: 3d81aa7838 1f9484f50e
Author: hendriktews <[email protected]>
Commit: GitHub <[email protected]>
Merge pull request #793 from hendriktews/kill-question
proof-shell: Don't ask about killing the proof assistant on exit
---
CHANGES | 5 +++++
generic/proof-shell.el | 6 ++++++
2 files changed, 11 insertions(+)
diff --git a/CHANGES b/CHANGES
index 8e77207399..6f5c3e0d5e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -19,6 +19,11 @@ the Git ChangeLog, the GitHub repo
https://github.com/ProofGeneral/PG
changes below for more details.
*** New command `proof-check-annotate' to annotate all failing proofs
with FAIL comments.
+*** Improve splash screen, add menu entry to permanently disable it
+ (Proof-General -> Quick Options -> Display -> Disable Splash Screen),
+ reduce splash screen time to make it less annoying
+*** Don't ask about killing the proof assistant when quitting Emacs and
+ thereby the Proof General session.
** Coq changes
*** support Coq 8.19
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 159711b912..c99c344ea8 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -479,6 +479,12 @@ process command."
(erase-buffer)
(proof-shell-set-text-representation)
+ ;; If the user quits Emacs together with the Proof General
+ ;; session, it's clear that the proof assistant needs to be
+ ;; killed - don't ask.
+ (set-process-query-on-exit-flag
+ (get-buffer-process proof-shell-buffer) nil)
+
;; Initialise associated buffers
(with-current-buffer proof-response-buffer
(erase-buffer)
