Zulip Chat Archive
Stream: PR reviews
Topic: 3285: reorder imports
Yury G. Kudryashov (Jul 07 2020 at 03:49):
#3285 reorders imports so that data.set.basic imports 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 02 2025 at 03:31 UTC