From b33bafb753e8512d3cf9b88c4fc30d0f3367683c Mon Sep 17 00:00:00 2001 From: Michael Hoennig Date: Fri, 13 Sep 2024 13:57:39 +0200 Subject: [PATCH] git-pull-and-run-if-origin-changed: pull every 10s and show commit-ids --- bin/git-pull-and-if-origin-changed-run-tests | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/bin/git-pull-and-if-origin-changed-run-tests b/bin/git-pull-and-if-origin-changed-run-tests index 7eb86a66..b1742689 100755 --- a/bin/git-pull-and-if-origin-changed-run-tests +++ b/bin/git-pull-and-if-origin-changed-run-tests @@ -12,7 +12,7 @@ while true; do # check if the local branch differs from the remote branch if [ "$LOCAL" != "$REMOTE" ]; then - echo "pulling changes from origin" + echo "local $LOCAL differs from remote $REMOTE => pulling changes from origin" git pull origin $BRANCH # run the command @@ -23,6 +23,7 @@ while true; do echo "no changes detected on the origin branch" fi - echo "waiting for 1 minute before checking again..." - sleep 60 + echo -e "waiting for changes..." + sleep 10 + echo -e "\r\033[K" done