Same behavior.
FWIW I run "git prune" immediately prior to "git push", _every_ time I
push to master.kernel.org (git.kernel.org).
Jeff
--
To unsubscribe from this list: send the line "unsubscribe git" in
the body of a message to majordomo@vger.kernel.org
More majordomo info at http://vger.kernel.org/majordomo-info.html