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
