Skip to content

Commit

Permalink
scripts: Handle remote URL change in update_deps.py
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
MathiasMagnus committed Oct 28, 2024
1 parent c21cdf4 commit c855f5e
Showing 1 changed file with 8 additions and 1 deletion.
9 changes: 8 additions & 1 deletion scripts/update_deps.py
Original file line number Diff line number Diff line change
Expand Up @@ -415,8 +415,15 @@ def Checkout(self):
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()
Expand Down

0 comments on commit c855f5e

Please sign in to comment.