Pulling from GitHub is slower than pulling from a local machine so I have a mirror set up. Cron keeps it mostly up to date. Dev machine then ran:
git clone git://server/llvm-project.git
git remote set-url --push origin git@github.com:llvm/llvm-project.git
So pushes always go to GitHub and pulls hit locally. Works fine until server is unavailable, e.g. because I don't have a VPN running.
I'd like to detect when server is unavailable, elegantly if possible but I'll just check the local IP if not, and have it fetch from GitHub directly in that case.
How do I configure this, and can it be done in secondary fallback fashion or must I change the upstream then change it back?
Thanks!
Equivalent but maybe simpler - happy with pull from local cache, then regardless of whether that worked, pull from GitHub. That's somewhat better in that it handles server lagging GitHub too.