Pull 1019

[Brad Roberts]

On Fri, 18 Jan 2013, monarch_dodra wrote:

> On Friday, 18 January 2013 at 18:35:47 UTC, Namespace wrote:
> > Ok, thanks.
> > But nobody can tell me when and if the "pull" is merged, right?
> > I think many users here would be pleased if someone could say something to
> > this pull.
> 
> Not sure what you mean?
> 
> Nobody will tell you when your pull fails the unittests.
> 
> When your pull actually gets merged for real into the "head", you aren't
> notified either (sadly), but the puller usually leaves a "merged" comment, and
> you get *that* notification.

Actually, github _does_ send a notification when the pull is merged.  They 
added that some time ago.