diff options
author | 1999-09-21 14:31:09 +0000 | |
---|---|---|
committer | 1999-09-21 14:31:09 +0000 | |
commit | 4cffebeb11d5b2f02a6c26a7f4d40a90181586fc (patch) | |
tree | 8b1b2e746bc3dead3c8ed1625c0fccd8ee457714 /generic | |
parent | ccb6578324ca1c41340d532a32fc21036aee7576 (diff) |
Callback for proof-shell-done-invisible now runs proof-state-change-hook.
Diffstat (limited to 'generic')
-rw-r--r-- | generic/proof-shell.el | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 3571b1d1..3adfbdf7 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1418,8 +1418,9 @@ May be called by proof-shell-invisible-command." (defun proof-shell-done-invisible (span) - "Callback for proof-shell-invisible-command. Do nothing." - ()) + "Callback for proof-shell-invisible-command. +Calls proof-state-change-hook." + (run-hooks 'proof-state-change-hook)) ;; FIXME da: I find the name of this command misleading. ;; Nothing much is invisible really. Old docstring was |