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.

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

fix: improve directory fallback on Linux and trim local time identifier #6221

Merged
merged 3 commits into from
Nov 27, 2024

Conversation

algebraic-dev
Copy link
Contributor

@algebraic-dev algebraic-dev commented Nov 26, 2024

This PR fixes:

  • Problems in other linux distributions that the default tzdata directory is not the same as previously defined by ensuring it with a fallback behavior when directory is missing.
  • Trim unnecessary characters from local time identifier.

@algebraic-dev algebraic-dev self-assigned this Nov 26, 2024
@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 26, 2024
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Nov 26, 2024

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0eca3bd55de7f29320e90b83ef2f43e9dff7546b --onto 20acc72a29a8bb4d55223651caa0553ffa82ac88. (2024-11-26 03:26:25)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0eca3bd55de7f29320e90b83ef2f43e9dff7546b --onto 9a17919ef11c2dba824498229633b8333a0b53d9. (2024-11-26 13:13:04)

@algebraic-dev algebraic-dev added this pull request to the merge queue Nov 27, 2024
Merged via the queue into leanprover:master with commit 88e3a2b Nov 27, 2024
14 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants