From 6fbc181914c721a5a3ce079f2eba80ee1b1124a5 Mon Sep 17 00:00:00 2001 From: Richard Copley Date: Fri, 23 Feb 2024 07:41:39 +0000 Subject: [PATCH] Don't permanently change Emacs standard-output. (#46) The macro lean4-with-info-output-to-buffer sets the Emacs global dynamic variable standard-output to the specified buffer, and doesn't set it back to its original value. This can cause other Emacs programs to go wrong subsequently. For example, "package.el" assumes that standard-output has its default value, so after using lean4-mode, it is impossible to update Emacs packages. This commit limits the duration of the change of standard-output by using let instead of setq. --- lean4-info.el | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lean4-info.el b/lean4-info.el index 35b6f5a..e5cdcb4 100644 --- a/lean4-info.el +++ b/lean4-info.el @@ -60,8 +60,8 @@ (with-current-buffer buf (setq buffer-read-only nil) (erase-buffer) - (setq standard-output buf) - ,@body + (let ((standard-output buf)) + ,@body) (setq buffer-read-only t)))) (defun lean4-ensure-info-buffer (buffer)