2012/12/23 Michael Raskin <[email protected]>: >>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 _______________________________________________ nix-dev mailing list [email protected] http://lists.science.uu.nl/mailman/listinfo/nix-dev
