echo "Adding remote '$2' to '$1'."
git remote add -t master "$2" "$3/$1"
git fetch "$2" > /dev/null
+ # Remove the remote and abort if the fetch was unsuccessful.
+ if [ "$?" -ne "0" ]; then
+ git remote rm "$2"
+ exit 1
+ fi
+
# Pushing to the remote pushes only the master branch in remotes named
# the hostname of this machine. This makes it easy to see where
# changes came from.
fi
# Merge with remote master if the repository was just created, otherwise
- # the repository starts empty.
+ # the repository starts empty. Also run gc to compress the new repository.
if [ $new = yes ]; then
git merge "$2/master"
+ git gc > /dev/null
fi
# Go back to the starting directory.