delete remote branch

Simon Peyton-Jones simonpj at
Thu Sep 12 17:16:15 UTC 2013

I haven't a clue what this wip thread is about, but I hope that in due course someone may update the Git Wiki page, (or wherever) to describe common workflows.  I am regularly confused by submodules, and I have no clue about wip stuff.  (Probably some of it only needs to be known by super-users.)



|  -----Original Message-----
|  From: ghc-devs [mailto:ghc-devs-bounces at] On Behalf Of Herbert
|  Valerio Riedel
|  Sent: 12 September 2013 09:40
|  To: Geoffrey Mainland
|  Cc: ghc-devs at
|  Subject: Re: delete remote branch
|  Hello Geoffrey,
|  On 2013-09-11 at 22:29:04 +0200, Geoffrey Mainland wrote:
|  [...]
|  > Is there any chance we could get the wip namespace up and running soon?
|  Sure, I've enabled it right now (and we can change the "wip/"
|  branch-prefix lateron should we come up with a better naming); there's
|  only the problem that everytime you push a rebased commit, the email
|  notification will be re-run, and the script will think the rebased
|  commits are completely new; just take that into account when pushing a
|  rebased commit :-)
|  hth,
|    hvr
|  _______________________________________________
|  ghc-devs mailing list
|  ghc-devs at

More information about the ghc-devs mailing list