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