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

@@ -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" \