comparison extra/soundsoftware/update-external-repo.sh @ 1599:aea6f97ff27f dockerise

Fix hggit extension name for more recent versions

     echo "$$: Update successful, pulling into local repo at $local_repo"
     if [ ! -d "$local_repo" ]; then
 	"$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
 fi