docs: clarify that the lean module is for lean3 by zaz · Pull Request #8278 · doomemacs/doomemacs · GitHub | Latest TMZ Celebrity News & Gossip | Watch TMZ Live
Skip to content

docs: clarify that the lean module is for lean3 #8278

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

docs: clarify that the lean module is for lean3 #8278

wants to merge 1 commit into from

Conversation

zaz
Copy link
Contributor

@zaz zaz commented Feb 16, 2025

Lean 4 was released some time ago, so I was surprised to find the lean module installed lean3-mode. To avoid confusion, could we, at least for now, replace the cutesy message with a warning that the user is installing a mode for a deprecated language?

We could later add lean4 as a lean4 module. I don't think it makes sense to complicate things by adding support for both Lean 4 and Lean 3 in the same module, because the Lean 3 is deprecated and going to become increasingly niche.

Related: Lean 4 module, PR #7439

  • I searched the issue tracker and this hasn't been PRed before.
  • My changes are not on the do-not-PR list for this project.
  • My commits conform to Doom's git conventions.
  • Any relevant issues or PRs have been linked to.

@zaz zaz requested a review from a team as a code owner February 16, 2025 13:01
@hlissner hlissner added is:docs Pertains to the project's manual, output of help commands, or API documentation was:moved Is, was, or will be addressed elsewhere module:lang/lean Pertains to Doom's :lang lean module labels Feb 21, 2025
@hlissner hlissner marked this pull request as draft February 21, 2025 20:06
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
is:docs Pertains to the project's manual, output of help commands, or API documentation module:lang/lean Pertains to Doom's :lang lean module was:moved Is, was, or will be addressed elsewhere
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@zaz @hlissner

TMZ Celebrity News – Breaking Stories, Videos & Gossip

Looking for the latest TMZ celebrity news? You've come to the right place. From shocking Hollywood scandals to exclusive videos, TMZ delivers it all in real time.

Whether it’s a red carpet slip-up, a viral paparazzi moment, or a legal drama involving your favorite stars, TMZ news is always first to break the story. Stay in the loop with daily updates, insider tips, and jaw-dropping photos.

🎥 Watch TMZ Live

TMZ Live brings you daily celebrity news and interviews straight from the TMZ newsroom. Don’t miss a beat—watch now and see what’s trending in Hollywood.