Zulip Chat Archive

Stream: mathlib4

Topic: Zulip shortcuts

Yaël Dillies (Nov 16 2022 at 22:47):

What's the plan for PR links on Zulip (eg #11000)? Once we'll have switched to mathlib4, surely we will get bored of writing mathlib4#37... Will we break all existing links or mass edit all messages?

Jireh Loreaux (Nov 16 2022 at 22:48):

Is it even possible to mass edit messages?

Yaël Dillies (Nov 16 2022 at 22:48):

It is possible to mass move them at least.

Eric Wieser (Nov 16 2022 at 22:54):

We could add 4#37 as a less boring spelling

Eric Wieser (Nov 16 2022 at 22:55):

But this is probably a question for #Zulip meta

Mario Carneiro (Nov 17 2022 at 01:24):

I don't think changes to the linkifier affect already posted messages

Patrick Massot (Nov 17 2022 at 06:53):

Zulip has a web api for mass modification of messages and I think admins can edit any message

Mario Carneiro (Nov 17 2022 at 07:02):

No, even admins can't do everything. I am an admin and I cannot edit your message, nor can I see private streams or private messages.

Mario Carneiro (Nov 17 2022 at 07:03):

I think we can just change the linkifier in this case. No mass changes are needed.

Last updated: Dec 20 2023 at 11:08 UTC