On 10/8/2013 4:36 AM, Jacob Carlborg wrote:
On Oct 08, 2013, at 10:26 AM, Brad Roberts <[email protected]> wrote:
The fix was merely repushing the commit id of the previously head of master
back as the current head
of master. Something internal to github's management of pulls got confused at
that point. So far,
no response to my support request.
As I replied to Walter:
I've learned that what's show in pull requests on Github is not always 100%
accurate. I would suggest merging a pull request on a local machine and see
what changes it actually contains.
I've done that and it appears to not be a problem.
_______________________________________________
dmd-internals mailing list
[email protected]
http://lists.puremagic.com/mailman/listinfo/dmd-internals
