-
Notifications
You must be signed in to change notification settings - Fork 39
Open
Milestone
Description
Lean4-Mode has the feature to automatically detect the version and launch either lean(3)-mode or Lean4-Mode as needed.
Since both Lean version 3 as well as Lean(3)-Mode is deprecated, the benefit of this feature is small. Since the implementation of this feature is quite complex and extensive, it's not adequate to the burden on maintenance work.
As discussed on Zulip#Emacs > `lean4-autodetect-lean3` and cleanup, let's drop this feature.
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
No labels