The other thing I learned the hard way is not to #NNNNN-mention any issues
that aren't to be closed when then PR is merged.

On Wed, Mar 1, 2017 at 9:13 AM, Jack Moffitt <j...@metajack.im> wrote:

> It contains a cohesive description of the entire set of changes. It
> would be a shame to omit it. In the cases of a PR with a single
> commit, this is the same as the commit message by default I think, but
> perhaps we detect that and don't duplicate.
>
> jack.
>
> On Wed, Mar 1, 2017 at 7:41 AM, Kartikaya Gupta <kgu...@mozilla.com>
> wrote:
> > On Wed, Mar 1, 2017 at 6:02 AM, Simon Sapin <simon.sa...@exyr.org>
> wrote:
> >> The first message of a pull request is copied into the merge commit when
> >> bors/homu merges it.
> >
> > What was the rationale behind this, out of curiousity?
> >
> > Cheers,
> > kats
> > _______________________________________________
> > dev-servo mailing list
> > dev-servo@lists.mozilla.org
> > https://lists.mozilla.org/listinfo/dev-servo
> _______________________________________________
> dev-servo mailing list
> dev-servo@lists.mozilla.org
> https://lists.mozilla.org/listinfo/dev-servo
>
_______________________________________________
dev-servo mailing list
dev-servo@lists.mozilla.org
https://lists.mozilla.org/listinfo/dev-servo

Reply via email to