[Nix-dev] Can't understand how pull requests work

[Marco Maggesi]

2012/12/23 Michael Raskin <7c6f434c at mail.ru>:
>>I submitted this pull request last week
>>
>>https://github.com/NixOS/nixpkgs/pull/216
>>
>>I cannot understand how this request could be marked as merged and
>>closed by me (I don't have commit access on the nixpkgs project, i
>>think).
>>
>>Also I noticed that no commit is associated to this pull request.
>>Can someone enlighten what actually happened?
>
> I am not sure, but my working hypothesis would be that someone silently
> picked your commit into master without using GitHub UI.

Probably myself.  But what I don't understand is that github declares
that the commit has been merged from maggesi:master into NixOS:master.

> Now, you have asked to pull branch X which is now a subset of master,
> so there are no commits to show. Oh, but empty pull request can be
> closed, noticed Github. Hm, maggesi is the only user associated with
> request — let's declare that the request is closed by maggesi.

Yes, this make sense.

> Am I right that HOL Light _is_ updated in master?

My original commit was (by mistake) in the "master" branch of my
nixpkgs repo, which is probably a bad idea.

Anyway, now I resubmitted a pull request (from a different branch).

Thanks,
Marco