echo pull information

This commit is contained in:
Denis Lehmann 2023-11-02 11:48:56 +01:00
parent 742b1d5a5c
commit f8bad2700b

4
gis
View file

@ -120,7 +120,7 @@ if [ "$fetch" == true ]; then
repository_name=$(basename "$dir")
# Fetch all Git repositories in background
git fetch --prune --all 1> /dev/null 2> >(trap 'kill $! 2> /dev/null' INT TERM; sed "s/^/${text_bold}${text_blue}${repository_name}${text_reset} /" >&2) &
git fetch --prune --all 1> /dev/null 2> >(trap 'kill $! 2> /dev/null' INT TERM; sed "s/^/${text_bold}${text_blue}${repository_name}${text_reset} /") &
fetch_pids+=("$!")
done
@ -157,7 +157,7 @@ if [ "$pull" == true ]; then
# Get repository name
repository_name=$(basename "$dir")
git pull 1> /dev/null 2> >(trap 'kill $! 2> /dev/null' INT TERM; sed "s/^/${text_bold}${text_magenta}${repository_name}${text_reset} /" >&2) &
git pull > >(trap 'kill $! 2> /dev/null' INT TERM; sed "s/^/${text_bold}${text_magenta}${repository_name}${text_reset} /") &
pull_pids+=("$!")
done