From fae7cac7ef5accfcd112e14cc336180383f6f947 Mon Sep 17 00:00:00 2001
From: Xavier Garrido <xavier.garrido@gmail.com>
Date: Fri, 15 Feb 2013 17:33:50 +0100
Subject: [PATCH] hide push/popd message. make git pull working with older git
 version

---
 antigen.zsh | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/antigen.zsh b/antigen.zsh
index 189f0cd..f08bf45 100644
--- a/antigen.zsh
+++ b/antigen.zsh
@@ -210,11 +210,18 @@ antigen-revert () {
         local old_rev="$(--plugin-git rev-parse HEAD)"
         # Pull changes if update requested.
         --plugin-git pull
+        # If pull failed then try to pull directly from the clone directory
+        # In older version (1.8) of git the previous command seems not to work
+        if [ $? -ne 0 ]; then
+            pushd > /dev/null
+            git pull
+            popd > /dev/null
+        fi
         # Update submodules.
-        pushd
+        pushd > /dev/null
         cd "$clone_dir"
         git submodule update --recursive
-        popd
+        popd > /dev/null
         # Get the new revision.
         local new_rev="$(--plugin-git rev-parse HEAD)"
     fi
-- 
2.0.0