Marge has been stabilised

Richard Eisenberg rae at
Tue Feb 12 16:23:55 UTC 2019

> On Feb 12, 2019, at 10:51 AM, Matthew Pickering <matthewtpickering at> wrote:
> This can be quickly toggled on/off by typing the /wip quick command in
> a comment.

This is an interesting aside. I understand this to mean: If I make a comment (the same place that I would write a comment for humans) that consists solely of "/wip", then instead of posting anything to humans, the title of my MR changes, either adding "WIP: " or deleting that from the beginning.

Are there other such pieces of magic? Is there a place they are listed?

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>

More information about the ghc-devs mailing list