mathlib3
d20a8cd5 - chore(.github/workflows): update gh-get-current-pr (#18763)

Commit

2 years ago

chore(.github/workflows): update gh-get-current-pr (#18763) The test that this upgrade works ok is that the awaiting-CI label is removed

Author

alexjbest

Parents