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

chore: lake: add build log file path to warning #4356

Merged
merged 1 commit into from
Jun 5, 2024

Conversation

tydeu
Copy link
Member

@tydeu tydeu commented Jun 5, 2024

Adds the path to build log to the warning for a missing/invalid build log to help with debugging.

@tydeu tydeu enabled auto-merge June 5, 2024 04:34
@tydeu tydeu disabled auto-merge June 5, 2024 04:34
@tydeu tydeu added the will-merge-soon …unless someone speaks up label Jun 5, 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 Jun 5, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ce67d6ef9ea598d5bc7b7dd84985342ca3559db9 --onto 9d4696123693b2f0deee658b8021236e5168b4de. (2024-06-05 04:51:46)

@tydeu tydeu added this pull request to the merge queue Jun 5, 2024
Merged via the queue into leanprover:master with commit 9c079a4 Jun 5, 2024
13 checks passed
@tydeu tydeu deleted the lake/build-log-path branch June 5, 2024 19:51
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN will-merge-soon …unless someone speaks up
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants