From a4d28701d907c7b3b177c25d9047cdbb449a3d78 Mon Sep 17 00:00:00 2001 From: Christian Schwarz Date: Sun, 12 Nov 2017 13:33:34 +0100 Subject: [PATCH] docs: fix publish.sh script (was not pushing changes to master) --- docs/publish.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/publish.sh b/docs/publish.sh index e024016..b2fd749 100755 --- a/docs/publish.sh +++ b/docs/publish.sh @@ -64,5 +64,5 @@ pushd "$PUBLICDIR" echo "adding and commiting all changes in GitHub pages repo" git add -A git commit -m "$COMMIT_MSG" -#git push origin master +git push origin master