# HG changeset patch
# User Chris Cannam
# Date 1307266107 -3600
# Node ID d3af621ba9d4c744079706f846aeb5dd60a08ee9
# Parent  50fd9c6b93a9d326dce6fb6b0af47735acb136ed
Update the master branch via git pull master rather than git fetch (which doesn't merge any particular branch)

diff -r 50fd9c6b93a9 -r d3af621ba9d4 extra/soundsoftware/update-external-repo.sh
--- a/extra/soundsoftware/update-external-repo.sh	Tue May 10 12:00:10 2011 +0100
+++ b/extra/soundsoftware/update-external-repo.sh	Sun Jun 05 10:28:27 2011 +0100
@@ -68,7 +68,7 @@
     if [ -d "$project_repo_mirror/.hg" ]; then
 	hg --config extensions.convert= convert --datesort "$remote_repo" "$project_repo_mirror" && success=true
     elif [ -d "$project_repo_mirror/.git" ]; then
-	( cd "$project_repo_mirror" && git fetch "$remote_repo" ) && success=true
+	( cd "$project_repo_mirror" && git pull "$remote_repo" master ) && success=true
     else 
 	echo "$$: ERROR: Repo mirror dir $project_repo_mirror exists but is not an Hg or git repo" 1>&2
     fi