From 8d8ce9e9c5580df7aa49665b174004f35a88b72a Mon Sep 17 00:00:00 2001
From: "Philipp A. Hartmann" <pah@qo.cx>
Date: Sun, 13 Jul 2014 11:54:24 +0200
Subject: [PATCH] travis-doxygen.sh: don't ignore Doxygen push error

---
 build/travis-doxygen.sh | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/build/travis-doxygen.sh b/build/travis-doxygen.sh
index 239afb3..74fa528 100755
--- a/build/travis-doxygen.sh
+++ b/build/travis-doxygen.sh
@@ -111,8 +111,7 @@ gh_pages_push() {
 		echo "https://${GH_TOKEN}:@${GITHUB_HOST}" > ${HOME}/.git-credentials ; \
 		chmod go-rw ${HOME}/.git-credentials )
 	# push to GitHub
-	git push origin gh-pages || \
-		skip "GitHub pages update failed, temporarily ignored."
+	git push origin gh-pages
 }
 
 doxygen_install