From c8e1ed9551f9dcbf9ee79817b527b18c631b1969 Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Thu, 26 Mar 2015 12:42:02 -0400 Subject: [PATCH] feat(emacs/lean-input): add lean-input-export-translations-to-stdout --- src/emacs/lean-input.el | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/emacs/lean-input.el b/src/emacs/lean-input.el index 6c3752645..27232bfdd 100644 --- a/src/emacs/lean-input.el +++ b/src/emacs/lean-input.el @@ -1120,3 +1120,8 @@ leanprover.github.io/js/input-method.js" (insert (format "\"},\n" input)))) (insert "};"))) + +(defun lean-input-export-translations-to-stdout () + (lean-input-export-translations) + (with-current-buffer "*lean-translations*" + (princ (buffer-string))))