]> git.plutz.net Git - blast/commitdiff
keep external repo up to date
authorPaul Hänsch <paul@plutz.net>
Fri, 6 Sep 2019 09:38:30 +0000 (11:38 +0200)
committerPaul Hänsch <paul@plutz.net>
Fri, 6 Sep 2019 09:38:30 +0000 (11:38 +0200)
modules/remo2hbo.mk

index e4c3a2d55074b85e5bf0565d7552f940fc5c2844..d82278e7410220122a592e5315b960e615d4f44d 100644 (file)
@@ -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 $@)"