From: Paul Hänsch <paul@plutz.net>
Date: Fri, 6 Sep 2019 09:38:30 +0000 (+0200)
Subject: keep external repo up to date
X-Git-Url: https://git.plutz.net/?a=commitdiff_plain;h=67ebbcc02dd81d8c4b0dba55b1d8790ea786b261;p=blast

keep external repo up to date
---

diff --git a/modules/remo2hbo.mk b/modules/remo2hbo.mk
index e4c3a2d..d82278e 100644
--- a/modules/remo2hbo.mk
+++ b/modules/remo2hbo.mk
@@ -99,8 +99,9 @@ gummikraken_clone:
 	[ -d gummikraken/.git ] || git clone https://git.tools.f4.htw-berlin.de/phaensch/gummikraken.git "gummikraken/"
 
 gummikraken/: gummikraken_clone
+	-git -C $@ pull
 	-git -C $@ submodule init
-	git -C $@ submodule update --remote
+	-git -C $@ submodule update --remote
 
 teesock/teesock.arm: teesock/
 	make -C $< "$(notdir $@)"