ref: ea1f78d7ebd7ac4866c86152e1fc0c425522ca15
parent: dad47c641c4ed7e3e2fcc7a894a24cf9b051fb9d
author: Ori Bernstein <[email protected]>
date: Tue Apr 14 18:35:48 EDT 2020
Improve merge message: give command to merge.
--- a/pull
+++ b/pull
@@ -91,10 +91,10 @@
# need to merge.
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 @}+ echo git/merge $remote
}
exit diverged
}