On Oct 08, 2013, at 10:26 AM, Brad Roberts <[email protected]> wrote:
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.
--
/Jacob Carlborg
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.
--
/Jacob Carlborg
_______________________________________________ dmd-internals mailing list [email protected] http://lists.puremagic.com/mailman/listinfo/dmd-internals
