changeset 1599:aea6f97ff27f dockerise

Fix hggit extension name for more recent versions
author Chris Cannam
date Wed, 23 Aug 2017 11:32:31 +0100
parents 073a75bf07fb
children ed9c467ef922
files extra/soundsoftware/update-external-repo.sh
diffstat 1 files changed, 1 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/extra/soundsoftware/update-external-repo.sh	Wed Aug 23 11:32:17 2017 +0100
+++ b/extra/soundsoftware/update-external-repo.sh	Wed Aug 23 11:32:31 2017 +0100
@@ -125,7 +125,7 @@
 	"$hg" init "$local_repo"
     fi
     if [ -d "$project_repo_mirror/.git" ]; then
-	( cd "$local_repo" && "$hg" --config extensions.hggit= pull "$project_repo_mirror" ) && echo "$remote_repo" > "$successfile"
+	( cd "$local_repo" && "$hg" --config extensions.git= pull "$project_repo_mirror" ) && echo "$remote_repo" > "$successfile"
     else 
 	( cd "$local_repo" && "$hg" pull "$project_repo_mirror" ) && echo "$remote_repo" > "$successfile"
     fi