[lmi] Relocating a proprietary git repository

[Greg Chicares]

[This email serves only to document some rarely-used git commands
that I wouldn't want to have to look up again. Nobody need read it.]

The public lmi repository uses savannah as a central server.
It is accompanied by a proprietary repository of product data,
which has no central server. Today, for historical reasons,
we've set that repository's 'origin' to physical directory
  /opt/lmi/blessed/proprietary/
on each machine (which made sense for msw), and in each chroot
now that all development takes place on GNU/Linux. That has
become inconvenient now that we have multiple chroots: we'd
like them all to be synchronized, all the time, as though
there were a single central repository.

Therefore, we plan to replace each chroot's local
  /opt/lmi/blessed/proprietary/
with a directory on the host:
  /srv/cache_for_lmi/blessed/proprietary/
that is identity-mounted in every chroot.

I was mildly surprised, but of course pleased, to learn that
git allows us to add an additional 'origin':
  git remote set-url --add --push origin 
file:///srv/cache_for_lmi/blessed/proprietary/
After I did that in one up-to-date chroot, I pushed the
current production commit (which is not the latest commit)
to all origins, thus:
  git push origin 15f42742:master
and then, on the host, verified the desired outcome:

[state before pushing from chroot]

/srv/cache_for_lmi/blessed/proprietary[0]$ git rev-parse master                 
       
1eee98b09d044e1d13726a0f57751abb474a1ac6

[now push from chroot]

/srv/cache_for_lmi/blessed/proprietary[0]$ ls -di /
2 /

[yes, this is assuredly the host]

/srv/cache_for_lmi/blessed/proprietary[0]$ git rev-parse master
15f42742b196feed9530240099e5bcb7ea17339e

[and its master is now 15f42742 as intended]

Soon I'll recreate a production chroot on our corporate server
(I'm trying to get another few GiB of storage first, but it's
the middle of the night in Hyderabad right now). It will have
only one 'origin' URL (pointing through a mount to the redhat
host), so nobody should every have to do any of this manually
or even be aware of it.