Skip to content

chore: remove unused variable in FileMap.ofString #11986

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
Open
ericluap wants to merge 1 commit into
base: master
Choose a base branch
from
Open

chore: remove unused variable in FileMap.ofString #11986

ericluap wants to merge 1 commit into from

Conversation

@ericluap
Copy link
Contributor

@ericluap ericluap commented Jan 13, 2026

Removes the unused line variable in FileMap.ofString

@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 Jan 13, 2026
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Jan 13, 2026

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1cd6db15792cf7f7b5dba4f9f7b3a9cd8a1002cd --onto e56351da7ae15673a5bc2b83e7fb70e1fbd988ca. You can force Mathlib CI using the force-mathlib-ci label. (2026-01-13 05:07:12)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Jan 13, 2026

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 1cd6db15792cf7f7b5dba4f9f7b3a9cd8a1002cd --onto d92cdae8e901d3d9686f8c0e88a0371379c49dff. You can force reference manual CI using the force-manual-ci label. (2026-01-13 05:07:14)

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

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

@ericluap @leanprover-community-bot @leanprover-bot