Christopher Hoskin
Christopher Hoskin
@sebdah Any change of getting this merged? Python 2 is pretty dead now.
I'm very close to having a Debian/Ubuntu package ready: https://tracker.debian.org/pkg/pympress . A .desktop file would be good.
Package now available in Debian Testing (Bullseye): https://packages.debian.org/bullseye/pympress And Ubuntu 20.04 (Focal): https://packages.ubuntu.com/focal/pympress
I've uploaded Pympress 1.5.3 to Debian (bullseye) https://packages.debian.org/bullseye/pympress .Sorry for not attending to this before now.
Something seems to have changed with `to_End_injective.semiring` - possibly connected with #12182?
``` /- The `doc_blame` linter reports: -/ /- DEFINITIONS ARE MISSING DOCUMENTATION STRINGS: -/ -- algebra/hom/centroid.lean #check @centroid_hom.to_add_monoid_hom /- def missing doc string -/ Error: centroid_hom.to_add_monoid_hom - def missing doc...
> ``` > /- The `doc_blame` linter reports: -/ > /- DEFINITIONS ARE MISSING DOCUMENTATION STRINGS: -/ > -- algebra/hom/centroid.lean > #check @centroid_hom.to_add_monoid_hom /- def missing doc string -/ >...
@eric-wieser Are you able to approve this now?
@eric-wieser Sorry to pester you again, but I was wondering if you might have a moment to approve this PR? Thanks.
This PR has an approval, and all of the comments appear to have been resolved. Please can I have delegated permission to merge it @eric-wieser ?