From aff3d410b2bbeb2dc47f79bd91326bdcd439306d Mon Sep 17 00:00:00 2001
From: Mike Gerwitz <mike@mikegerwitz.com>
Date: Tue, 8 May 2012 19:10:43 -0400
Subject: [PATCH] webdoc will now use origin/master by default - More sensical
 for CI where master may not be up to date - Can be overridden with
 WEBDOC_BRANCH

---
 tools/webdoc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/webdoc b/tools/webdoc
index 5984b74..0f887ae 100755
--- a/tools/webdoc
+++ b/tools/webdoc
@@ -97,7 +97,7 @@ webify()
 }
 
 # generate the documentation from the master branch
-git checkout master \
+git checkout "${WEBDOC_BRANCH:-origin/master}" \
   && make doc-html \
   && git checkout - \
     && webify "$path_doc_single" \