Zulip Chat Archive
Stream: PR reviews
Topic: !4#4020 CategoryTheory.DifferentialObject
Ruben Van de Velde (Jun 13 2023 at 13:12):
This is green now if you want to put it on the queue, @Scott Morrison
Yury G. Kudryashov (Jun 14 2023 at 04:17):
Post-merge comment: I think that we should #align fields of structures if we rename them.
Yury G. Kudryashov (Jun 14 2023 at 04:17):
Added #align in !4#5033 (help wanted)
Last updated: Dec 20 2023 at 11:08 UTC