diff --git a/.github/deploy.sh b/.github/deploy.sh index 6cebbb7801b0c..ea118a3b6fce5 100644 --- a/.github/deploy.sh +++ b/.github/deploy.sh @@ -8,6 +8,7 @@ rm -rf out/master/ || exit 0 echo "Making the docs for master" mkdir out/master/ cp util/gh-pages/index.html out/master +cp util/gh-pages/theme.js out/master cp util/gh-pages/script.js out/master cp util/gh-pages/style.css out/master diff --git a/util/gh-pages/index_template.html b/util/gh-pages/index_template.html index d942cbe39e72d..f052e95cdafd4 100644 --- a/util/gh-pages/index_template.html +++ b/util/gh-pages/index_template.html @@ -26,6 +26,7 @@
+