max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(emacs/lean-project): remove old project file contents

Browse source
This commit is contained in:
Gabriel Ebner 2017-01-18 08:56:47 +01:00 • committed by Leonardo de Moura
parent 9530a7db1c
commit 9b63ceff91
1 changed files with 1 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/emacs/lean-project.el
View file

@ -23,22 +23,10 @@
(interactive
(list (read-directory-name "Specify the project root directory: ")))
(let ((project-file (concat (file-name-as-directory directory)
lean-project-file-name))
(ext "lean")
(default-contents
(s-join "\n"
;; EXT is a placeholder.
'("# Lean project file"
""
"# Include all .EXT files under this directory"
"+ *.EXT"
""
"# Exclude emacs temp files"
"- .#*.EXT"))))
lean-project-file-name)))
(if (file-exists-p project-file)
(user-error "project-file %s already exists" project-file))
(find-file project-file)
(insert (s-replace "EXT" ext default-contents))
(save-buffer)))
(provide 'lean-project)