* admin/update_autogen (commit): Pull before push.

diff --git a/admin/update_autogen b/admin/update_autogen
index 898432eae6047613ea0ee45bd2acaec89cbad4a6..9393ab0ee907cf56da368ff522ae192dc078431c 100755 (executable)
--- a/admin/update_autogen
+++ b/admin/update_autogen
@@ -237,6 +237,8 @@ commit ()
     $vcs commit -m "; Auto-commit of $type files." "$@" || return $?
 
     [ "$vcs" = "git" ] && {
+        ## In case someone else pushed something while we were working.
+        $vcs pull --rebase || return $?
         $vcs push || return $?
     }