Commit a44df22f authored by Cyril Brulebois's avatar Cyril Brulebois

Avoid duplicating hostname and home directory.

parent 2343a373
......@@ -11,7 +11,10 @@ tools_repo=debian/xsf-tools.git
# Some blurb to make everything work:
cp mrconfig.head $mrconfig
sed \
-e "s,@@host@@,$host,g" \
-e "s,@@home@@,$home,g" \
mrconfig.head > $mrconfig
# Build a list of repositories based on the actual repositories on the
# server:
......@@ -6,7 +6,7 @@ checkout =
repo_dir=$(echo "$MR_REPO"|sed -e "s,$here,," -e "s,/$,,");
repo_name=$(basename $repo_dir);
git clone git://$repo_dir $repo_name
git clone git://@@host@@@@home@@/$repo_dir $repo_name
# Avoid the default 'git pull' and all the merges that come with it:
update =
......@@ -14,6 +14,6 @@ update =
# Make it easy to switch from git:// to ssh:// so that one can push:
git2ssh =
sed -i 's,git://,ssh://,' $MR_REPO/.git/config
sed -i 's,git://@@host@@,ssh://@@host@@,' $MR_REPO/.git/config
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment