mirror of
https://github.com/zrepl/zrepl.git
synced 2025-06-20 01:37:45 +02:00
diff: actually fix publish.sh script
This commit is contained in:
parent
9e9f464de7
commit
73d586f305
2
docs/.gitignore
vendored
2
docs/.gitignore
vendored
@ -1 +1 @@
|
|||||||
public
|
public_git
|
||||||
|
@ -3,7 +3,7 @@ set -eo pipefail
|
|||||||
|
|
||||||
GHPAGESREPO="git@github.com:zrepl/zrepl.github.io.git"
|
GHPAGESREPO="git@github.com:zrepl/zrepl.github.io.git"
|
||||||
SCRIPTDIR=$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )
|
SCRIPTDIR=$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )
|
||||||
PUBLICDIR="${SCRIPTDIR}/public"
|
PUBLICDIR="${SCRIPTDIR}/public_git" #use different dir than default dir 'public' (hugo server -D)
|
||||||
|
|
||||||
checkout_repo_msg() {
|
checkout_repo_msg() {
|
||||||
echo "checkout ${GHPAGESREPO} to ${PUBLICDIR}:"
|
echo "checkout ${GHPAGESREPO} to ${PUBLICDIR}:"
|
||||||
@ -39,17 +39,17 @@ git fetch origin
|
|||||||
git reset --hard origin/master
|
git reset --hard origin/master
|
||||||
|
|
||||||
echo "cleaning GitHub pages repo"
|
echo "cleaning GitHub pages repo"
|
||||||
git clean -dn
|
git rm -rf .
|
||||||
|
|
||||||
popd
|
popd
|
||||||
|
|
||||||
echo "building site"
|
echo "building site"
|
||||||
hugo
|
hugo -d "$PUBLICDIR"
|
||||||
|
|
||||||
pushd "$PUBLICDIR"
|
pushd "$PUBLICDIR"
|
||||||
|
|
||||||
echo "adding and commiting all changes in GitHub pages repo"
|
echo "adding and commiting all changes in GitHub pages repo"
|
||||||
git add -A
|
git add -A
|
||||||
git commit -m "hugo render from publish.sh - `date -u`"
|
git commit -m "hugo render from publish.sh - `date -u`" #TODO include parent commit id
|
||||||
git push origin master
|
git push origin master
|
||||||
|
|
||||||
|
Loading…
x
Reference in New Issue
Block a user