Skip to content
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

chore: add newline at end of file for lake new templates #6026

Merged
merged 1 commit into from
Nov 13, 2024
Merged

chore: add newline at end of file for lake new templates #6026

merged 1 commit into from
Nov 13, 2024

Conversation

alissa-tung
Copy link
Contributor

@alissa-tung alissa-tung commented Nov 11, 2024 •
edited by tydeu
Loading

This PR adds a newline at end of each Lean file generated by lake new templates.

I have tested it with a locally compiled Lean with this commit. I hope these changes make lake new's behavior more consistent with the Lean 4 plugins and libraries newlines convention.

@alissa-tung alissa-tung requested a review from tydeu as a code owner November 11, 2024 04:16
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Nov 11, 2024
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Nov 11, 2024 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 48e3d7617386ea44c92999afc2b555f3e6cb6ecd --onto 811d8fb3c01cf5724ba4daf733898793cca24bdd. (2024-11-11 04:34:57)
  • ✅ Mathlib branch lean-pr-testing-6026 has successfully built against this PR. (2024-11-11 05:56:38) View Log

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 11, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6026
81c2a40
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 11, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6026
2ac1b06
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Nov 11, 2024
@tydeu tydeu added this pull request to the merge queue Nov 12, 2024
@tydeu
Copy link
Member

tydeu commented Nov 12, 2024

LGTM! Thanks!

@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to no response for status checks Nov 12, 2024
@tydeu tydeu enabled auto-merge November 12, 2024 21:41
@tydeu tydeu added this pull request to the merge queue Nov 12, 2024
@kmill kmill removed this pull request from the merge queue due to a manual request Nov 13, 2024
@tydeu tydeu added this pull request to the merge queue Nov 13, 2024
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to no response for status checks Nov 13, 2024
@tydeu tydeu added this pull request to the merge queue Nov 13, 2024
Merged via the queue into leanprover:master with commit d5adadc Nov 13, 2024
20 checks passed
@alissa-tung alissa-tung deleted the patch-1 branch November 14, 2024 09:20
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@tydeu tydeu Awaiting requested review from tydeu tydeu is a code owner

Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@alissa-tung @leanprover-community-bot @tydeu