> I don't think this problem is really serious. > If the push fails, you can just commit (locally) a new changeset that > repairs the EOL or indentation problems
I would find that unfortunate. It's a fairly irrelevant change, yet it may manage to corrupt the history (hg blame). > and push the whole bunch of > changesets again (I assume the server-side hook will not examine > changesets individually, but only the last of them?). That is for us to decide. I can see arguments either way. But it shouldn't happen often that the server refuses a push; all errors should already be caught on the clients. Regards, Martin _______________________________________________ Python-Dev mailing list Python-Dev@python.org http://mail.python.org/mailman/listinfo/python-dev Unsubscribe: http://mail.python.org/mailman/options/python-dev/archive%40mail-archive.com