Something I learned the hard way is to avoid a sentence like this one: "Does not fix #123."
Github will dutifully detect "fix #123" and close the corresponding issue. =) On Wed, Mar 1, 2017 at 10:21 AM, Alan Jeffrey <[email protected]> wrote: > 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 _______________________________________________ dev-servo mailing list [email protected] https://lists.mozilla.org/listinfo/dev-servo
