2023-05-28 09:53:19 +02:00
|
|
|
#!/bin/bash
|
2023-05-28 11:26:17 +02:00
|
|
|
repository_name=${GITHUB_REPOSITORY#*/}
|
|
|
|
|
if [[ $repository_name == *.github.io ]]; then
|
|
|
|
|
echo "Name ends with github.io"
|
|
|
|
|
else
|
|
|
|
|
echo "Name does not end with github.io, not generating pages"
|
2023-06-05 20:54:11 +02:00
|
|
|
exit
|
2023-05-28 09:53:19 +02:00
|
|
|
fi
|
|
|
|
|
|
|
|
|
|
npm install
|
2023-06-05 20:54:11 +02:00
|
|
|
node pages.js
|
2023-05-28 09:53:19 +02:00
|
|
|
|
2023-06-15 23:26:44 +02:00
|
|
|
set -e
|
2023-05-28 11:34:56 +02:00
|
|
|
pushd docs
|
2023-05-28 09:53:19 +02:00
|
|
|
git add *
|
|
|
|
|
git commit -am "Updated $(date +'%Y-%m-%d')"
|
|
|
|
|
git push
|
|
|
|
|
popd
|
