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 <[email protected]> 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 <[email protected]> > wrote: > > On Wed, Mar 1, 2017 at 6:02 AM, Simon Sapin <[email protected]> > 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 > > [email protected] > > https://lists.mozilla.org/listinfo/dev-servo > _______________________________________________ > dev-servo mailing list > [email protected] > https://lists.mozilla.org/listinfo/dev-servo > _______________________________________________ dev-servo mailing list [email protected] https://lists.mozilla.org/listinfo/dev-servo
