Zulip Chat Archive

Stream: new members

Topic: New PR

Josha Dekker (Dec 16 2023 at 15:20):

I just made a pull request but somehow I linked it to an existing chore? Not sure what went wrong, should I make a new fresh PR, or is this one fine? (Assuming that it builds?...)

https://github.com/leanprover-community/mathlib4/pull/9107

Yaël Dillies (Dec 16 2023 at 15:20):

Note: You can type #9107 to the same effect :smile:

Yaël Dillies (Dec 16 2023 at 15:21):

To fix your PR, can you git fetch; git merge origin/master on your branch?

Josha Dekker (Dec 16 2023 at 15:21):

That's good to hear, I assumed it would, but was afraid it wouldn't! Thanks for the confirmation!

Josha Dekker (Dec 16 2023 at 15:22):

yes, what should the message read?

Josha Dekker (Dec 16 2023 at 15:25):

I just did it, named it "fix: mistake pull request"

Last updated: Dec 20 2023 at 11:08 UTC