On Mon, 12 Sep 2011, Paul E. McKenney wrote: > PS. If someone knows how to make github delete a branch, please let me > know, as this would allow me to use the "rcu/next" nomenclature. > Yes, it is probably obvious, but I am new to github... git push origin :branch should work everywhere, right? -- Jiri Kosina SUSE Labs -- To unsubscribe from this list: send the line "unsubscribe linux-next" in the body of a message to majordomo@xxxxxxxxxxxxxxx More majordomo info at http://vger.kernel.org/majordomo-info.html
