+gdb_7_2-branch

diff --git a/bin/master-UPDATE b/bin/master-UPDATE
index 220df3d..4accf89 100755 (executable)
--- a/bin/master-UPDATE
+++ b/bin/master-UPDATE
@@ -1,7 +1,7 @@
 #! /bin/bash
 set -ex
 git fetch gdb
-for i in master;do     # gdb_7_1-branch
+for i in master gdb_7_2-branch;do      # gdb_7_1-branch
        git checkout $i
        [ "`git status|head -n1`" = "# On branch $i" ]
        git pull origin