Add identifiers

This commit is contained in:
Caspar Jungbacker 2023-04-17 18:41:26 +02:00
parent c36c2abd80
commit 3ff3d78469

View file

@ -37,11 +37,12 @@ push-html:
before_script:
- apt-get update -y
- apt-get install rsync -y
- git remote add origin https://gitlab-ci-token:$ACCESS_TOKEN@gitlab.tudelft.nl/$CI_PROJECT_PATH.git
- git config --global user.name "$GITLAB_USER_NAME"
- git config --global user.email "$GITLAB_USER_EMAIL"
- git fetch origin publish-html
- git checkout publish-html
script:
- rsync -av --delete book/_build/html/* ./.
- git add --all -- ':!book/*' ':!.cache/*'
- git commit -m "$CI_COMMIT_MESSAGE"
- git push origin publish-html
- git push https://gitlab-ci-token:$ACCESS_TOKEN@gitlab.tudelft.nl/$CI_PROJECT_PATH.git publish-html