Split SERVER into REMOTE_USER/HOST/HOME, rename USER_REPO to REPO

This commit is contained in:
2026-06-13 21:06:48 +02:00
parent 596b94519f
commit bc3df5c24b
3 changed files with 13 additions and 9 deletions
+2 -2
View File
@@ -2,7 +2,7 @@
set -e
: "${WEBROOT:?WEBROOT is not set}"
: "${USER_REPO:?USER_REPO is not set}"
: "${REPO:?REPO is not set}"
: "${GITEA_HOST:?GITEA_HOST is not set}"
: "${GITEA_USER:?GITEA_USER is not set}"
: "${GITEA_TOKEN:?GITEA_TOKEN is not set}"
@@ -18,7 +18,7 @@ echo "==> Cloning user repo"
printf 'machine %s\nlogin %s\npassword %s\n' "$GITEA_HOST" "$GITEA_USER" "$GITEA_TOKEN" > ~/.netrc
chmod 600 ~/.netrc
rm -rf user
git clone "$USER_REPO" user
git clone "$REPO" user
rm ~/.netrc
echo "==> Setting permissions"