Zulip Chat Archive
Stream: PR reviews
Topic: std4#314
Yuyang Zhao (Nov 15 2023 at 12:16):
I can't change the label of std4#314. Also there still seems to be no consensus on renaming docs#Nat.bit.
Mario Carneiro (Nov 15 2023 at 12:18):
comment awaiting-review on the PR to change the label
Last updated: Dec 20 2023 at 11:08 UTC