From 399bb95065238507df50cf09fc9d10ead0d01176 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 1 Sep 2017 14:25:00 +0200 Subject: [PATCH] chore(emacs/lean-dev): fix lean-diff-test-file --- src/emacs/lean-dev.el | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/emacs/lean-dev.el b/src/emacs/lean-dev.el index 0b4f6c50ab..6bc6dcb64d 100644 --- a/src/emacs/lean-dev.el +++ b/src/emacs/lean-dev.el @@ -11,6 +11,6 @@ (interactive) (message (shell-command-to-string (format "yes | ./test_single.sh \"%s\" \"%s\" yes" (lean-get-executable "lean") - (buffer-name))))) + (buffer-file-name))))) (provide 'lean-dev)