Zulip Chat Archive
Stream: PR reviews
Topic: notation for units #11236
Johan Commelin (Jan 05 2022 at 12:24):
This passed CI.
Kevin Buzzard (Jan 05 2022 at 15:54):
LGTM!
Oliver Nash (Jan 05 2022 at 15:58):
Any reason not to merge this immediately?
Oliver Nash (Jan 05 2022 at 15:59):
(115 files changed)
Johan Commelin (Jan 05 2022 at 16:56):
I kicked it on the queue, since I got a bors d+.
Last updated: Dec 20 2023 at 11:08 UTC