mathlib3
[Merged by Bors] - fix: handle archive and counterexamples correctly when adding port comments
#19237
Closed
Overview
Commits
1
Changes
View On GitHub

[Merged by Bors] - fix: handle archive and counterexamples correctly when adding port comments #19237

eric-wieser wants to merge 1 commit into master from fix-port-comments
eric-wieser
eric-wieser fix: handle archive and counterexamples correctly when adding port co…
c1903690
eric-wieser eric-wieser added CI
eric-wieser eric-wieser added awaiting-CI
eric-wieser eric-wieser removed awaiting-CI
eric-wieser eric-wieser added awaiting-review
kim-em kim-em added not-too-late
kim-em
github-actions github-actions added ready-to-merge
github-actions github-actions removed awaiting-review
bors
bors bors changed the title fix: handle archive and counterexamples correctly when adding port comments [Merged by Bors] - fix: handle archive and counterexamples correctly when adding port comments 2 years ago
bors bors closed this 2 years ago
bors bors deleted the fix-port-comments branch 2 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
No reviews
Assignees
No one assigned
Labels
ready-to-merge CI not-too-late
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum