search

leanprover / lean3-mode

Emacs mode for Lean
Apache License 2.0
69 stars 17 forks source link

lean-mode-required-packages variable #3

Closed arademaker closed 7 years ago

arademaker commented 7 years ago

after install the package and restart Emacs I got:

Symbol's value as variable is void: lean-mode-required-packages

Any idea?

Kha commented 7 years ago

This variable was part of the old setup for Lean mode. You can remove that code from you Emacs init file now.