fix a bug in the ./all script when checking out the DP repo

diff --git a/all b/all
index b8e59d63cfa8d39f5b70eb6510596092c3b225d7..e49faeb823f2c6a24597c97f5bcdd2b3f2ade727 100755 (executable)
--- a/all
+++ b/all
@@ -233,7 +233,9 @@ case "$cmd" in
                        else
                                verbose git clone "$url" "$d0/$d"
                                enter "$d0/$d" verbose
-                               verbose git checkout "$branch"
+                               if [ "$branch" != "master" ]; then
+                                       verbose git checkout --track -b "$branch" origin/"$branch"
+                               fi
                                cd "$d0"
                        fi
                done