Can't edit my own PR titles

Stream: mathlib4

[Jeremy Tan]

I've noticed this since a few days ago and I don't know why this change has happened. Can someone fix it?

[Robin Arnez]

Weird, this might be a github change? I think you can still edit the title though if go to Files changed -> Preview (top right) -> Switch to classical experience -> Edit

[Robin Arnez]

Oh, https://github.com/orgs/community/discussions/186398

[Jeremy Tan]

Switching back to the old PR viewer does work

[Robin Arnez]

Really? Are you on the Files changed tab? The button disappears on any other tab

[Jeremy Tan]

Yes, I am on the Files Changed tab

[Jeremy Tan]

Of course it disappears on other tabs

[Robin Arnez]

Okay well it seems like github cli still works? Maybe you can try that

[Jakub Nowak]

There's also another workaround, that doesn't require cli, mentioned in the linked github issue.

[Johan Commelin]

Is this still an issue? Seems like a regression to me. If needed, we can provide a command, so that writing

update-title chore(foobar): yadda xyzzy

in a comment will update the title.