Am 9/5/2013 11:18, schrieb Jørgen Edelbo: > Forgetting to push something that you have just > completed is very far from what I am used to. "Forgetting to push" is just one of many reasons why a branch that is not equal to HEAD is not yet pushed... The new restriction is just too tight. -- Hannes -- To unsubscribe from this list: send the line "unsubscribe git" in the body of a message to majordomo@xxxxxxxxxxxxxxx More majordomo info at http://vger.kernel.org/majordomo-info.html