Re: [HTCondor-devel] fetching github pull requests

[Tim Theisen <tim@xxxxxxxxxxx>]

This is already well documented on our wiki:

ÂÂÂ
https://htcondor-wiki.cs.wisc.edu/index.cgi/wiki?p=MergingGihubPullRequests

...Tim

On 4/24/19 3:31 PM, Carl Edquist wrote:
> Hi all,
>
> I was just discussing this with Jaime -
>
> If someone makes a github pull request against the htcondor mirror, it
> is not necessary to take the diffs and manually re-create commits
> locally. It is possible to fetch the commits directly for a github
> pull request down to your local git repository.
>
> You can set up a separate remote for this in your local condor repo, eg:
>
> ÂÂÂÂ$ git remote add PR https://github.com/htcondor/htcondor
> ÂÂÂÂ$ git config remote.PR.fetch "+refs/pull/*/head:refs/remotes/PR/*"
> ÂÂÂÂ$ git fetch PR
>
> This will create a remote called "PR", and, for example, you can
> access the commit for github pull request 23 as "PR/23". You can pass
> that in as an argument to gitk, git-diff, git-checkout, git-merge, etc.
>
> If you want to merge a PR into master (or whatever branch the PR
> submitter requested), you can do that with:
>
> ÂÂÂÂ$ git merge PR/23
>
> and when push your changes back to the main AFS repo, then github will
> see the PR got merged and mark it as merged/closed.
>
>
> If you get tired of having all the remote PR refs in your local git
> repo, you can remove them all simply by removing the remote:
>
> ÂÂÂÂ$ git remote rm PR
>
>
> Hopefully you may find this useful,
>
> Carl

-- 
Tim Theisen
Release Manager
HTCondor & Open Science Grid
Center for High Throughput Computing
Department of Computer Sciences
University of Wisconsin - Madison
4261 Computer Sciences and Statistics
1210 W Dayton St
Madison, WI 53706-1685
+1 608 265 5736