From 7abc9b3da73c980c07717b62c215894344c97259 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Dachary?= <loic@dachary.org>
Date: Sat, 2 Jul 2022 14:32:25 +0200
Subject: [PATCH] use pull instead of fetch

Otherwise the working directory is not updated and it will lead to
diverging branches
---
 infrastructure/utils.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/infrastructure/utils.py b/infrastructure/utils.py
index 45393a5..42bb231 100644
--- a/infrastructure/utils.py
+++ b/infrastructure/utils.py
@@ -224,7 +224,7 @@ class Infra:
         )
 
     def _pull(self):
-        self.repo.git.fetch(env=self.env)
+        self.repo.git.pull(env=self.env)
 
     # TODO: switch to using Git cmd