Restart distccd on a clean batch-pull.

diff --git a/tools/make-git b/tools/make-git
index 8104efd2b2992fdf970fcc25644b49cd2e23a95a..5a3fed4a5a75c084b393af0e3f216f52d0b373f8 100644 (file)
--- a/tools/make-git
+++ b/tools/make-git
@@ -49,6 +49,7 @@ git_pull() {
        if [ "$1" = "--batch" ]; then
                shift
                git pull $* | grep -q "Already up-to-date." || rm -f $FAILED
+               [ -e $FAILED ] || distccd_restart
        else
                if [ "$CURRENT_BRANCH" == "master" ]; then
                        if ! (git status | grep -q "working directory clean"); then