git push --no-mirror ?

Hi,

I have a remote that I use mainly for backup with 'mirror = true' in gitconfig, but also for sharing my "bleeding-edge" code with a student. Now I came across the situation where I would liked to push only a single branch to that repo, only to discover that 'git push' has no '--no-mirror' option to override the related configuration setting. Removing the 'mirror = true' line from the config, doing the push, restoring the config did the trick, of course, but I think there should be a simpler way to do that. Is there a fundamental reason why there is no 'push --no-mirror', or just noone has noticed/bothered before?

Thanks, Gábor