diff --git a/.github/scripts/deploy b/.github/scripts/deploy index 539484a9..0347c004 100755 --- a/.github/scripts/deploy +++ b/.github/scripts/deploy @@ -1,8 +1,15 @@ -#!/bin/sh +#!/bin/sh -e # Deploys the User Guide to the production # website. Triggered by updates to the GitHub # repo's master branch. -cd "$REPO_DIRECTORY" +REPO=/opt/userguide +SITE=/home/public_html/userguides/userguide4 + +cd "$REPO" +git switch master git pull + +rm -rf "$SITE" +cp -R "$REPO/docs" "$SITE"