diff --git a/tools/deploy_docs.sh b/tools/deploy_docs.sh index f39cc023730..127a3831ea5 100644 --- a/tools/deploy_docs.sh +++ b/tools/deploy_docs.sh @@ -18,7 +18,7 @@ then git add dev git commit -m "Deployed to GitHub Pages" - git push --force --quiet "https://${GHTOKEN}@${GH_REF}" gh-pages > /dev/null 2>&1 + git push --force --quiet "https://${GH_TOKEN}@${GH_REF}" gh-pages > /dev/null 2>&1 ) else echo "-- will only push docs from master --"