From e71db7109dff266fd5b383019455c6338fedafe9 Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Wed, 5 Nov 2014 09:20:14 -0500 Subject: [PATCH] fix(emacs/lean-mode.el): remove quotation marks in lean-execute Close #294 --- src/emacs/lean-mode.el | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index 042bb7f1cb..25f50e4be8 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -32,7 +32,7 @@ (defun lean-compile-string (exe-name args file-name) "Concatenate exe-name, args, and file-name" - (format "\"%s\" %s \"%s\"" exe-name args file-name)) + (format "%s %s %s" exe-name args file-name)) (defun lean-create-temp-in-system-tempdir (file-name prefix) "Create a temp lean file and return its name"