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

fix(emacs): bug in suggested Emacs init

Browse source 
The original code set the variable `lean-required-packages`, but then expected `lean-mode-required-packages`.

I've also added a hint about where to find your emacs init file; this was something I had to learn to follow these instructions.

A question for follow-up: the requirements sections states that `fill-column-indicator` is a dependency, but the suggested init file does not attempt to install this. Should this be fixed?
This commit is contained in:
Scott Morrison 2017-01-02 22:58:15 +11:00 • committed by Leonardo de Moura
parent a85e89f555
commit 54ee157fa9
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/emacs/README.md
View file

@ -65,13 +65,13 @@ Installation
============
You can also include lean-mode permanently in your emacs init file. In this
case, just put the following code in your Emacs init file:
case, just put the following code in your Emacs init file (typically `~/.emacs.d/init.el`):
```elisp
;; You need to modify the following two lines:
(setq lean-rootdir "~/projects/lean")
(setq lean-emacs-path "~/projects/lean/src/emacs")
(setq lean-required-packages '(company dash dash-functional f
(setq lean-mode-required-packages '(company dash dash-functional f
flycheck let-alist s seq))
(require 'package)