Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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.
- Loading branch information