Skip to content

[Merged by Bors] - feat: set pp.mvars.anonymous false for MathlibTest #205298

[Merged by Bors] - feat: set pp.mvars.anonymous false for MathlibTest

[Merged by Bors] - feat: set pp.mvars.anonymous false for MathlibTest #205298

Triggered via pull request July 24, 2026 13:22
@joneugsterjoneugster
submitted #42016
Status Success
Total duration 9s
Artifacts

labels_from_comment.yml

on: pull_request_review
update-label
4s
update-label
Fit to window
Zoom out
Zoom in