Non maintainer review

Stream: mathlib4

[Etienne Marion]

I reviewed #16713, and it seems all right to me, there's just a small indentation issue which I wrote about while "approving the changes" (not sure what this really means). Should I leave it as it is, or should I maintainer merge (I don't know if I'm allowed/supposed to)?

[Ruben Van de Velde]

We appreciate the help, but I'm afraid that if you're not a reviewer, "maintainer merge" won't do anything. You can either just "approve" in the github UI or also mention that you did in the #PR reviews stream, which might convince a reviewer or maintainer to look earlier than they otherwise might

[Ruben Van de Velde]

(Not feeling confident to approve it myself, but I left one small comment as well)

[Etienne Marion]

All right, thanks for the answer!

[Patrick Massot]

Maybe this isn’t clear in Ruben’s explanation, but reviewing and approving PRs is very much appreciated by the maintainer team in all cases.

[Yaël Dillies]

Yes, it is just that you can't maintainer merge, but we will certainly take your review into account (and it will help!)

[Ruben Van de Velde]

That's what I tried to start with, but thanks for clarifying :)

[Etienne Marion]

No problem I had understood :smiley: