scripts: Handle remote URL change in update_deps.py

Without going through an intricate dance with git to change the remote
URL of a repository, it's simplest to just nuke the cloned folder, as
we have to do a clean clone anyway.

1 files changed, 8 insertions, 1 deletions

diff --git a/scripts/update_deps.py b/scripts/update_deps.py
index d010f9b2..24d125a9 100755
--- a/scripts/update_deps.py
+++ b/scripts/update_deps.py
@@ -415,8 +415,15 @@ class GoodRepo(object):
         if VERBOSE:
             print('Checking out {n} in {d}'.format(n=self.name, d=self.repo_dir))
 
-        if self._args.do_clean_repo:
+        if os.path.exists(os.path.join(self.repo_dir, '.git')):
+            url_changed = command_output(['git', 'config', '--get', 'remote.origin.url'], self.repo_dir).strip() != self.url
+        else:
+            url_changed = False
+
+        if self._args.do_clean_repo or url_changed:
             if os.path.isdir(self.repo_dir):
+                if VERBOSE:
+                    print('Clearing directory {d}'.format(d=self.repo_dir))
                 shutil.rmtree(self.repo_dir, onerror = on_rm_error)
         if not os.path.exists(os.path.join(self.repo_dir, '.git')):
             self.Clone()