ignore errors of git fetch --tag as this fails on a case-insensitive filesystem like...
authorThierry Parmentelat <thierry.parmentelat@inria.fr>
Sat, 30 Apr 2022 17:12:30 +0000 (19:12 +0200)
committerThierry Parmentelat <thierry.parmentelat@inria.fr>
Sat, 30 Apr 2022 17:33:36 +0000 (19:33 +0200)
module-tools.py

index e9f3096..85e4e3e 100755 (executable)
@@ -199,7 +199,7 @@ class GitRepository:
             self.__run_command_in_repo("git checkout {}".format(branch))
         else:
             self.to_branch(branch, remote=True)
-        self.__run_command_in_repo("git fetch origin --tags")
+        self.__run_command_in_repo("git fetch origin --tags", ignore_errors=True)
         self.__run_command_in_repo("git fetch origin")
         if not self.__is_commit_id(branch):
             # we don't need to merge anything for commit ids.