.github/workflows/push_pr.yml

chore: remove `ToMathlib/Height`, which has been upstreamed #531

Sign in to view logs

Triggered via pull request November 21, 2024 19:58

synchronize #186

grunweg:MR-height-upstreamed

Status Success

Total duration 8m 42s

Artifacts –

push_pr.yml

on: pull_request