>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. 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. Am I right that HOL Light _is_ updated in master? _______________________________________________ nix-dev mailing list [email protected] http://lists.science.uu.nl/mailman/listinfo/nix-dev
