Trivial DMD fixes: GitHub pull requests vs. Bugzilla issues

[David Nadlinger]

On 3/20/11 12:20 AM, Jonathan M Davis wrote:
> Bugzilla is for tracking bugs. github is for tracking the source. So, in
> general, I would expect bugs to be reported to bugzilla.  I would guess though,
> that enhancement requests aren't quite as critical if you already have a patch
> for them (though you're likely to get a better discussion on bugzilla if you
> post enhancements there in addition to creating a pull request). However, given
> that this sounds like a very small change, it's probably fine that it's just a
> pull request - though, of courses, Walter would be better suited to say what
> Walter would prefer.

Funny, that's actually a pretty accurate description of what I was 
thinking when I asked the question. ;)

> Regardless, as I understand it, Walter has been a bit overwhelmed with pull
> requests of late (you can check out the thread on dmd-internals about it:
> http://lists.puremagic.com/pipermail/dmd-internals/2011-March/001293.html ), and
> it's taking him some time to work through them. I expect that he'll get to your
> pull request eventually.

Oh, I just noticed that I must have messed up my dmd-internals 
subscription somehow, not noticing it because I got the commit 
notifications directly via GitHub nevertheless (but wondering why it was 
so quiet lately) – thanks a lot!

David