On 3 June 2014 21:08, Daniel James
It doesn't work for me either, but it does work for 'archive'. Which is a bit odd, maybe 'clone' uses the setting from the config file so that future commands in that repo will work consistently. We could set HOME to another directory which contains a config file with the settings we need. Or we could something similar to my script for the documentation. Are you using python? I use a shell script for the documentation build, but I should be able to convert it to python.
I've attached a script which creates a mirror and exports a couple of copies under the directory it is in. This behaviour is at the end, it should be easy to modify. I think I'm going to use this for a new version of the documentation build setup, the current shell script is getting unwieldy.