diff options
| author | Serial <69764315+Serial-ATA@users.noreply.github.com> | 2022-04-26 18:22:37 -0400 |
|---|---|---|
| committer | Serial <69764315+Serial-ATA@users.noreply.github.com> | 2022-04-26 18:22:37 -0400 |
| commit | 06cc1abbb1b64a60c059137b3d610bbe0e0f3bea (patch) | |
| tree | 40d69adbb724a04fb40b77bb957dbc89d54a6dfc /.github/deploy.sh | |
| parent | bdc896165928de3e04b02f3f5632094fe337ebbc (diff) | |
Move js out to its own file
Diffstat (limited to '.github/deploy.sh')
| -rw-r--r-- | .github/deploy.sh | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/.github/deploy.sh b/.github/deploy.sh index 34225a54029..5a59f94ec91 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/script.js out/master cp util/gh-pages/lints.json out/master if [[ -n $TAG_NAME ]]; then |
