# HG changeset patch
# User Chris Cannam
# Date 1307361186 -3600
# Node ID 4eb486dbf73041dd0800f71b953d3ab3ff0e83de
# Parent  897979555864fbef4806a87ed6abdf098637c7f2
If the remote repo URL changes, move aside the existing local mirror and start afresh.
(Not yet tested: checkpointing this prior to working on a different aspect of the problem)

diff -r 897979555864 -r 4eb486dbf730 extra/soundsoftware/update-external-repo.sh
--- a/extra/soundsoftware/update-external-repo.sh	Mon Jun 06 10:58:52 2011 +0100
+++ b/extra/soundsoftware/update-external-repo.sh	Mon Jun 06 12:53:06 2011 +0100
@@ -60,6 +60,27 @@
 
 success=""
 
+# If we have a record of the last successfully updated remote repo
+# URL, check it against our current remote URL: if it has changed, we
+# will need to start again with a new clone rather than pulling
+# updates into the existing local mirror
+
+successfile="$project_mirror/last_successful_url"
+if [ -f "$successfile" ]; then
+    last=$(cat "$successfile")
+    if [ x"$last" == x"$remote_repo" ]; then
+	echo "$$: Remote URL is unchanged from last successful update"
+    else
+	echo "$$: Remote URL has changed since last successful update:"
+	echo "$$: Last URL was $last, current is $remote_repo"
+	suffix="$$.$(date +%s)"
+	echo "$$: Moving existing repos to $suffix suffix and starting afresh"
+	mv "$project_repo_mirror" "$project_repo_mirror"."$suffix"
+	mv "$local_repo" "$local_repo"."$suffix"
+	mv "$successfile" "$successfile"."$suffix"
+    fi
+fi
+
 if [ -d "$project_repo_mirror" ]; then
 
     # Repo mirror exists: update it
@@ -96,12 +117,12 @@
 
 if [ -n "$success" ]; then
     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
-	if [ ! -d "$local_repo" ]; then
-	    "$hg" init "$local_repo"
-	fi
-	( cd "$local_repo" && "$hg" --config extensions.hggit= pull "$project_repo_mirror" )
+	( cd "$local_repo" && "$hg" --config extensions.hggit= pull "$project_repo_mirror" ) && echo "$remote_repo" > "$successfile"
     else 
-	( cd "$local_repo" && "$hg" pull "$project_repo_mirror" )
+	( cd "$local_repo" && "$hg" pull "$project_repo_mirror" ) && echo "$remote_repo" > "$successfile"
     fi
 fi