> From: Sergio Durigan Junior <sergiodj@redhat.com> > Cc: brobecker@adacore.com, gdb-patches@sourceware.org > Date: Thu, 28 Feb 2019 15:17:02 -0500 > > Just as a reminder, these changes need to be pushed to origin/master as > well. Yes, I usually push to master and then cherry-pick to the branch. I believe this is the procedure?