Yes, please go ahead and remove these branches. On Mon, May 21, 2018 at 8:06 PM, Vlad Rozov <vro...@apache.org> wrote:
> There is an option to delete the branch on github directly (no need to > use "git push"). > > Thank you, > > Vlad > > > On 5/21/18 18:35, Boaz Ben-Zvi wrote: > >> I mistakenly pushed a branch (“MERGE-180521-01”) into the Apache >> repo, and plan to delete it soon >> (i.e. do “git push https://github.com/apache/drill.git --delete >> MERGE-180521-01” ). >> >> Just in case someone notices .... >> >> On this occasion: Looks like there are other similar such branches: >> “DRILL-3478” and “DRILL-4235” ; any objection to deleting those as well ? >> >> Thanks, >> >> Boaz >> >> >> >
