Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
chore: pr-release.yaml: fetch nightly-with-mathlib sha using ls-remote
this refines upon #3834, which didn’t quite work, and was producing ``` From https://github.com/leanprover/lean4 * branch nightly-with-mathlib -> FETCH_HEAD * [new branch] nightly-with-mathlib -> origin/nightly-with-mathlib fatal: ambiguous argument 'nightly-with-mathlib': unknown revision or path not in the working tree. ``` Probably `git -C lean4.git fetch origin nightly-with-mathlib:nightly-with-mathlib` would have worked, or using `rev-parse origin/nightly-with-mathlib`. We now get the commit hash via `git ls-remote`, which I’d wager is a bit more robust, as it is independent of the local state.
- Loading branch information