| Age | Commit message (Collapse) | Author |
|---|
|
The way this script was previously working is that
we define several DESTINATIONs with one acting
as a default. The destination for git pushes can
be changed via command line option, but all pushes
are still sent to the same location.
We have a situation with an android mirror where we do
*not* want to push it through gerrit as it is served
only via gitolite. Since the upstream contains around
1060 repos, we prefer to push it straight to disk and
leave gerrit out instead of creating a huge load for
the server.
This change allows us to specify the repo_root variable
in a host section to bypass the default DESTINATION.
Change-Id: Ibbb5470b632e29598f4a8d1e77b1b9d955067755
|
|
Thus, it resolves issue with where seed manifest comes from, and how to
keep it up to date.
Change-Id: I9e0458a9120d2b72d8d4d405d367037ca180e3d5
|
|
Sometimes different downstream projects may need different mirrors of the
same upstream tree. So, just allow to have different mirroring entries for
the same host, differentiated with "#slug".
Change-Id: I8a2edd0a58e22965ab896d3c5839623b0f844840
|
|
Change-Id: I9e74ab5ad21c7ce4dd2a48250eb224d879400982
|
|
Change-Id: I964a7691c010e41b2e8e1d08ab624938aff4c860
|
|
Actual config is now managed by Ansible in ansible-playbooks.git .
Change-Id: If895fca2b1b6c6b8148a9707ba893fcec01e8f04
|
