Stream: PR reviews
Topic: 3285: reorder imports
Yury G. Kudryashov (Jul 07 2020 at 03:49):
imports so that
order.bounded_lattice. It touches 22 files, so I'd prefer to have it merged or declined before it rots.
Johan Commelin (Jul 07 2020 at 04:38):
It's on the queue now.
Last updated: May 06 2021 at 12:15 UTC