Zulip Chat Archive

Stream: mathlib4

Topic: !4#3490 Urysohns Lemma

Lucas Viana (Apr 18 2023 at 02:37):

Hi everyone, I just ported my first mathlib file (Topology.UrysohnsLemma) but forgot to ask here for repo permissions first. Before that I checked the Zulip channel and existing PRs and it seemed like nobody was working on it. The PR should be ready for review now, but due to my mistake I can't assign labels to it.

Scott Morrison (Apr 18 2023 at 02:40):

Thanks, @Lucas Viana --- I've just invited you to the repository.

Lucas Viana (Apr 18 2023 at 02:40):

Thanks!

Jeremy Tan (Apr 18 2023 at 02:50):

@Scott Morrison the protect_proj/protected issue you pointed out has been fixed, it can be merged

Jeremy Tan (Apr 18 2023 at 02:56):

@Lucas Viana are you there?

Lucas Viana (Apr 18 2023 at 02:56):

Hi, yes

Jeremy Tan (Apr 18 2023 at 02:56):

Please comment bors r+ on your PR

Lucas Viana (Apr 18 2023 at 02:57):

I see. I was just reading the bors instructions before doing that

Scott Morrison (Apr 18 2023 at 03:17):

Jeremy Tan said:

Lucas Viana are you there?

Patience, @Jeremy Tan! :-)

Last updated: Dec 20 2023 at 11:08 UTC