<html><body><div>On Oct 08, 2013, at 10:26 AM, Brad Roberts <braddr@puremagic.com> wrote:<br><br><div><blockquote type="cite"><div class="msg-quote"><div class="_stretch"> The fix was merely repushing the commit id of the previously head of master back as the current head <br> of master. Something internal to github's management of pulls got confused at that point. So far, <br> no response to my support request.</div></div></blockquote><span></span><br>As I replied to Walter:<br><br>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.<br><br>--<br>/Jacob Carlborg<br></div></div></body></html>