Run update server info after deleting a remote branch

diff --git a/update b/update
index 7eb5ffcba2b4087591949db022256efec58c863b..34ed844ff2ed728dc09439028471622a11acd215 100755 (executable)
--- a/update
+++ b/update
@@ -21,7 +21,7 @@ git pull --ff-only current master &&
 web="`git config --get --path remote.web.url`" &&
 if [ -n "$web" ]; then
    git push web &&
-   cd "$web" && git branch -dr current/master
+   cd "$web" && git branch -dr current/master && git update-server-info
 fi &&
 
 cd "$current" && exec git pull origin