Merge pull request #14 from ndw/master

Restore master branch after publishing website
docbook · Jul 15, 2020 · aa8a3bd · aa8a3bd
2 parents 97e8107 + 348d2c2
commit aa8a3bd
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/.circleci/publish-website.sh b/.circleci/publish-website.sh
@@ -45,3 +45,6 @@ rm /tmp/website.$$.tar.gz
 git add .
 git commit -m "Deploy gh-pages for ${CIRCLE_PROJECT_USERNAME}: ${SHA}"
 git push -q origin HEAD
+
+# Go back to the master branch
+git checkout master