diff options
| author | Jan Holthuis <jan.holthuis@ruhr-uni-bochum.de> | 2020-12-16 23:04:24 +0100 |
|---|---|---|
| committer | Jan Holthuis <jan.holthuis@ruhr-uni-bochum.de> | 2020-12-16 23:04:24 +0100 |
| commit | ea64072eaff399b9a28c08f32ebefa02d808e9df (patch) | |
| tree | 9dd798818e1694a80c8070690bad6e2f1373b6eb /tools | |
| parent | 5503b8ff989a70a885452deb251536c8bca40dd4 (diff) | |
GitHub Actions: Re-add inconvenient per-OS subdirectory to deploy path
Diffstat (limited to 'tools')
| -rwxr-xr-x | tools/deploy.sh | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tools/deploy.sh b/tools/deploy.sh index 6cc95ceb6f..328f160ac3 100755 --- a/tools/deploy.sh +++ b/tools/deploy.sh @@ -9,11 +9,12 @@ set -eu -o pipefail [ -z "${SSH_PASSWORD}" ] && echo "Please set the SSH_PASSWORD env var." >&2 && exit 1 [ -z "${SSH_USER}" ] && echo "Please set the SSH_USER env var." >&2 && exit 1 [ -z "${UPLOAD_ID}" ] && echo "Please set the UPLOAD_ID env var." >&2 && exit 1 +[ -z "${OS}" ] && echo "Please set the OS env var." >&2 && exit 1 [ -z "${DESTDIR}" ] && echo "Please set the DESTDIR env var." >&2 && exit 1 SSH="ssh -i ${SSH_KEY} -o StrictHostKeyChecking=no -o UserKnownHostsFile=/dev/null" GIT_BRANCH="$(git rev-parse --abbrev-ref HEAD)" -DEST_PATH="${DESTDIR}/${GIT_BRANCH}" +DEST_PATH="${DESTDIR}/${GIT_BRANCH}/${OS}" TMP_PATH="${DESTDIR}/.tmp/${UPLOAD_ID}" echo "Deploying to $TMP_PATH, then to $DEST_PATH." |