www-infrastructure-dev mailing list archives

Site index · List index
Message view « Date » · « Thread »
Top « Date » · « Thread »
From Paul Davis <paul.joseph.da...@gmail.com>
Subject Re: Git pull requests
Date Tue, 24 Jul 2012 18:01:14 GMT
On Tue, Jul 24, 2012 at 12:37 PM, Jeremy Thomerson
<jeremy@thomersonfamily.com> wrote:
> On Mon, Jul 23, 2012 at 11:52 AM, Paul Davis
> <paul.joseph.davis@gmail.com> wrote:
>> On Sat, Jul 21, 2012 at 10:54 PM, Jeremy Thomerson
>> <jeremy@thomersonfamily.com> wrote:
>>> Jukka, et al,
>>>
>>>   I can't remember - so sorry if I am just forgetting - but I thought
>>> that when we got pull requests and merged them in that GitHub would
>>> automatically close the pull request. But I pulled one a couple weeks
>>> ago and it didn't close.  Is there something we can/need to do to
>>> close pull requests?
>>>
>>> Here's the pull req: https://github.com/apache/wicket/pull/16
>>> I used this (from the email) to pull it in:     $ git pull
>>> https://github.com/jesselong/wicket for-apache-master-pr-2
>>> And the commit is in our repo:
>>> https://github.com/apache/wicket/commit/83740b9e5f9ca91ae185bc5683b6c94a5349b85b
>>>
>>> Thanks!
>>> Jeremy Thomerson
>>
>> I don't see that commit on master. Not sure if I'm just missing it but
>> I think that's a requirement for the PR to be closed automatically.
>
> It's there: https://github.com/apache/wicket/commits/master?page=2
>
> Jeremy

Ah. Not sure then. I wonder if GH has docs on the specifics for auto
closing PR's.

Mime
View raw message