ref: dad47c641c4ed7e3e2fcc7a894a24cf9b051fb9d
parent: 65e7c353bca28ba6bf0b4cceb387373e853e628a
author: Ori Bernstein <ori@eigenstate.org>
date: Tue Apr 14 17:55:33 EDT 2020
allow 'git/pull' to fetch all branches
--- a/pull
+++ b/pull
@@ -15,8 +15,11 @@
upstream=$2
url=$3
dir=$4
-
- {git/fetch -b $branch -u $upstream $url >[2=3] || die $status} | awk '+ bflag=()
+ if(~ $#branch)
+ bflag=(-b $branch)
+ echo git/fetch $branch -u $upstream $url
+ {git/fetch $bflag -u $upstream $url >[2=3] || die $status} | awk ' /^remote/{if($2=="HEAD")
next
@@ -52,6 +55,8 @@
case -b
branch=$2
shift
+ case -a
+ branch=()
case -f
checkout=()
case -i
@@ -84,8 +89,15 @@
}
# The remote repository and our HEAD have diverged: we
# need to merge.
-if(! ~ `{git/query HEAD $remote @} `{git/query HEAD})- die 'remote diverged:' $remote
+if(! ~ `{git/query HEAD $remote @} `{git/query HEAD}){+ >[1=2]{+ echo remote diverged: $remote
+ echo ours: `{git/query HEAD}+ echo theirs: `{git/query $remote}+ echo common: `{git/query HEAD $remote @}+ }
+ exit diverged
+}
# The remote is directly ahead of the local, and we have
# no local commits that need merging.
echo $remote':' `{git/query $local} '=>' `{git/query $remote} >[1=2]--
⑨