You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
First change (in lean4-lake-find-dir in "lean4-lake.el"):
I agree with the change but I also wonder if anyone would notice if we deleted "lean4-lake.el". We could just mention in the README that building happens automatically when lake is started as a server, and direct users to the compile command if they do need to run lake build.
Second change (in lean4-find-files in "lean4-util.el"):
lean4-find-files and lean4--collect-entries are unused and should be deleted.
Third change (in lean4-get-executable in "lean4-util.el"):
The change depends on Emacs 28.1, but I think it's worth supporting 27.1 a while longer unless we have a more compelling reason. If I'm reading the docs right, 27.1 is the default on Debian oldstable (bullseye) and Ubuntu 22.04.
The change depends on Emacs 28.1, but I think it's worth supporting 27.1 a while longer unless we have a more compelling reason. If I'm reading the docs right, 27.1 is the default on Debian oldstable (bullseye) and Ubuntu 22.04.
In #51, @akirak made some suggestions that were deemed out of the scope of that PR. Go over these suggestions and decide whether to implement them.
The text was updated successfully, but these errors were encountered: