[dmd-internals] Fixing github pull requests that I borked up

[Walter Bright]

On 10/8/2013 4:36 AM, Jacob Carlborg wrote:
> On Oct 08, 2013, at 10:26 AM, Brad Roberts <braddr at puremagic.com> 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.