diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-01-04 17:14:29 +0100 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-01-04 17:14:29 +0100 |
| commit | 15b977ff32f6c8250d47d7657987b0c94db76710 (patch) | |
| tree | 7f70c0855d99fe7d37f784fc45e763ee9afa383b /generic/proof-config.el | |
| parent | af30e1ef04320547273fa02967ddcdb18f380f12 (diff) | |
| parent | 8d405f342bb3a1903fc12184f78f191e7d84c29d (diff) | |
Merge remote-tracking branch 'OFFICIAL/master'
Diffstat (limited to 'generic/proof-config.el')
| -rw-r--r-- | generic/proof-config.el | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index b4898a35..8ce53168 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1683,7 +1683,12 @@ tries to interrupt the proof process. It is therefore run earlier than `proof-shell-handle-error-or-interrupt-hook', which runs when the interrupt is acknowledged inside `proof-shell-exec-loop'. -This hook also runs when the proof assistent is killed." +This hook also runs when the proof assistent is killed. + +Hook functions should set the dynamic variable `prover-was-busy' +to t if there might have been a reason to interrupt. Otherwise +the generic interrupt handler might issue a prover-not-busy +error." :type '(repeat function) :group 'proof-shell) |