git push --no-mirror ?

["SZEDER Gábor" <szeder@ira.uka.de>]

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