Zulip Chat Archive

Stream: mathlib4

Topic: PR name

Iván Renison (Jan 17 2026 at 22:08):

Hi, in #34085 the PR title formatting is failing and I don't understand why. Does somebody sees what I have wrong in the title?

Ruben Van de Velde (Jan 17 2026 at 22:27):

Weird, it seems fine when trying to reproduce locally

Ruben Van de Velde (Jan 17 2026 at 22:28):

Oh, there was a space at the start

Ruben Van de Velde (Jan 17 2026 at 22:29):

I wonder if we could make that clearer, cc @Michael Rothgang

Iván Renison (Jan 17 2026 at 22:30):

Ah, ok, I didn't saw the space, thank you

Michael Rothgang (Jan 28 2026 at 09:49):

Yes, we can: #34518 should improve the error reporting (and adds a few more checks).

Last updated: Feb 28 2026 at 14:05 UTC