diff options
| -rw-r--r-- | generic/proof-script.el | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 373efc8c..50a718bb 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -588,8 +588,7 @@ NAME does not need to be unique." (pg-make-element-visible idiom (symbol-name key)))))) (proof-with-script-buffer ; may be called from menu - (maphash alterfn elts))) - (pg-redisplay-for-gnuemacs)) + (maphash alterfn elts)))) ;; Next two could be in pg-user.el. No key-bindings for these. (defun pg-show-all-proofs () |