From c50ab524a594ed707080fef00792641bd872318d Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Fri, 4 Mar 2016 15:18:45 -0500 Subject: [PATCH] fix(emacs/lean-project.el): update prompt message, have standard as a defualt close #1017 --- src/emacs/lean-project.el | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/emacs/lean-project.el b/src/emacs/lean-project.el index 679f7cb2a..911ccd9cc 100644 --- a/src/emacs/lean-project.el +++ b/src/emacs/lean-project.el @@ -19,15 +19,15 @@ (defun lean-project-create (directory type) (interactive (list (read-directory-name "Specify the project root directory: ") - (intern (completing-read "Project type:: " '(standard hott))))) + (intern (completing-read "Project type (standard or hott): " '(standard hott) nil t)))) (let ((project-file (concat (file-name-as-directory directory) lean-project-file-name)) (ext (pcase type - (`lean "lean") (`standard "lean") - (`hlean "hlean") (`hott "hlean") - (_ (error "Unknown project type %S. Please select either standard or hott" type)))) + (_ (progn + (message "Default 'standard' lean-project is created.") + "lean")))) (default-contents (s-join "\n" ;; EXT is a placeholder.