diff --git a/utils/push_subtrees.sh b/utils/push_subtrees.sh index fb430d5f9da57f08c7c52810b31bbfe400b18eae..b4949ea2dca1465c2cc0282d59442c158d7138e1 100755 --- a/utils/push_subtrees.sh +++ b/utils/push_subtrees.sh @@ -26,7 +26,12 @@ if [[ $depsCount > 0 ]]; then echo "---- Push ${aDeps[$i, name]} ----" # Push le dépôt - git subtree push --prefix src/${aDeps[$i, name]} "git@gitlab.veremes.net:Development/vitis_apps/sources/${aDeps[$i, name]}.git" master + + { # 'try' block + git subtree push --prefix src/${aDeps[$i, name]} "git@gitlab.veremes.net:Development/vitis_apps/sources/${aDeps[$i, name]}.git" master + } || { # 'catch' block + echo "could not push ${aDeps[$i, name]}" + } fi done fi