The other thing that I just noticed can be a problem is that it is not
clear if a closed pull request is closed because it was merged or
because a better patch was needed (unless the pull was exactly merged,
in which case it says "merged" at the top). So if you are closing a
pull request for whate
On Wed, Apr 6, 2011 at 9:03 AM, Vinzent Steinberg
wrote:
> On 6 Apr., 00:32, Ondrej Certik wrote:
>> > I think the suggestion is to not open a new one but to reopen the same one.
>>
>> Yes.
>
> Alright, this definitely makes sense. The only drawback I see is that
> we can't tell the difference be
On 6 Apr., 00:32, Ondrej Certik wrote:
> > I think the suggestion is to not open a new one but to reopen the same one.
>
> Yes.
Alright, this definitely makes sense. The only drawback I see is that
we can't tell the difference between a closed unfinished and a closed
finished pull request easily.
On Tue, Apr 5, 2011 at 2:30 PM, Aaron Meurer wrote:
> On Tue, Apr 5, 2011 at 8:37 AM, Vinzent Steinberg
> wrote:
>> On 4 Apr., 22:26, Ondrej Certik wrote:
>>> The pull requests should be used only for code, that the author thinks
>>> is *ready* to go in. So people will comment, and more work wil
On Tue, Apr 5, 2011 at 8:37 AM, Vinzent Steinberg
wrote:
> On 4 Apr., 22:26, Ondrej Certik wrote:
>> The pull requests should be used only for code, that the author thinks
>> is *ready* to go in. So people will comment, and more work will be
>> needed. That is ok, it will take a day or two, to po
On 4 Apr., 22:26, Ondrej Certik wrote:
> The pull requests should be used only for code, that the author thinks
> is *ready* to go in. So people will comment, and more work will be
> needed. That is ok, it will take a day or two, to polish this up. If
> it takes 3 weeks however, then I think the c
> By the way, another thing to remember about editing comments is that
> no notification is sent to anyone for an edited comment (I don't know
> if this applies if you add @username in an edit). Notifications are
> only send for new comments. So if you want someone to know you have
> commented on
On Apr 4, 2011, at 2:26 PM, Ondrej Certik wrote:
> On Mon, Apr 4, 2011 at 12:01 PM, Tom Bachmann wrote:
>> I try to update TODO as soon as I see comments, but usually the time
>> from leaving comments to me seeing them and updating TODO is much
>> longer than the time I need to address the comme
Hm, so either I am wrong, or there is a bug in GitHub (there is a bug either
way, because if you really can't edit other people's comments, it shouldn't let
you think you can). I have seen this myself, now that I think about it. Maybe
you should ask about it on GitHub support.
By the way, ano
On Mon, Apr 4, 2011 at 12:01 PM, Tom Bachmann wrote:
> I try to update TODO as soon as I see comments, but usually the time
> from leaving comments to me seeing them and updating TODO is much
> longer than the time I need to address the comments and re-set TODO to
> "nothing" (except if I postpone
I try to update TODO as soon as I see comments, but usually the time
from leaving comments to me seeing them and updating TODO is much
longer than the time I need to address the comments and re-set TODO to
"nothing" (except if I postpone work to later in the day for some
reason).
On 4 Apr., 15:13,
The closing and opening would work but then comments may be lost...or
maybe not. Even if a pull is closed you can still access it, right?
Aaron, I tried to edit the TODO on [ https://github.com/sympy/sympy/pull/183
] but after pressing Update Comment, the changes didn't stick.
--
You received th
On Sun, Apr 3, 2011 at 7:47 PM, Chris Smith wrote:
> Aaron S. Meurer wrote:
>>> Actually, any repo collaborator (i.e., anyone with push access to
>>> the repo) can edit *any* comment, regardless of who made it.
>>>
>>> I'm just wondering because I personally don't have any difficulty
>>> keeping t
Aaron S. Meurer wrote:
>> Actually, any repo collaborator (i.e., anyone with push access to
>> the repo) can edit *any* comment, regardless of who made it.
>>
>> I'm just wondering because I personally don't have any difficulty
>> keeping track of this stuff, so if others (like you) do, I'm
>> wo
Actually, any repo collaborator (i.e., anyone with push access to the repo) can
edit *any* comment, regardless of who made it.
I'm just wondering because I personally don't have any difficulty keeping track
of this stuff, so if others (like you) do, I'm wondering if you need me to keep
track of
One more thing...when new commits are added (in response to
suggestions) they get added below the previous comments so github is
actually helping the process in that regard:
commit
commit
commit
comments
comments
new commit <-- when you see this you know something new has been
added. That's a g
Only the person who made the request has edit privileges of the
comments, right? So they would summarize what needs to be done.
Another idea that came to me is that when a comment has been dealt
with, it could be deleted and the TODO comment could just say (as
someone did recently).
TODO
n
17 matches
Mail list logo
