Zulip Chat Archive
Stream: general
Topic: new steam for PR discussions
Scott Morrison (Oct 07 2018 at 10:26):
I've just created a new stream, after a brief discussion with Mario, for discussion of current PRs.
Patrick Massot (Oct 07 2018 at 10:27):
Let me cast the first vote: Merge #397 Now!
Scott Morrison (Oct 07 2018 at 10:27):
My main idea is that it is a place for everyone-besides-Mario-and-Johannes to ask each other for help and reviews, without it constituting nagging Mario-and-Johannes.
Scott Morrison (Oct 07 2018 at 10:28):
I think it would also be helpful if many more of us participated in reviews of PRs. (I'm certainly too lazy here.)
Scott Morrison (Oct 07 2018 at 10:29):
And hopefully it's okay for anyone to give a "positive review" of a PR --- simply chiming in that they've either looked at the changes and they seem good, or even better that they've tried them out in some way.
Scott Morrison (Oct 07 2018 at 10:29):
This should then make it easier for Mario and Johannes to deal with the easy ones that don't need significant input from them.
Mario Carneiro (Oct 07 2018 at 10:29):
/me approves
Patrick Massot (Oct 07 2018 at 10:37):
Yes, I did try 397, it works here. We only miss a VScode one key stroke trick to insert {!!} and Ctrl-.
Patrick Massot (Oct 07 2018 at 10:38):
Oh, it's merged now!
Patrick Massot (Oct 07 2018 at 10:38):
Thanks!
Rohan Mitta (Dec 11 2018 at 12:51):
I've redone my Banach's Contraction Theorem PR (#428) to use the material pointed out by Patrick, I think it's ready now!
Johan Commelin (Dec 11 2018 at 15:19):
@Rohan Mitta There is a separate stream for PR's as announced in this thread. I created a thread there for your PR.
Johan Commelin (Dec 11 2018 at 15:19):
Rohan Mitta (Dec 13 2018 at 13:38):
Whoops! Thanks Johan
Last updated: Dec 20 2023 at 11:08 UTC