Permalink
Browse files

Push documentation to docs folder instead of dev

  • Loading branch information...
thuijskens committed Sep 15, 2018
1 parent 77d15e6 commit 7bf34d740877ff70c05c716dcc535ead0e2226df
Showing with 1 addition and 1 deletion.
  1. +1 −1 ci_scripts/circleci/push_doc.sh
@@ -17,7 +17,7 @@ GENERATED_DOC_DIR=$(readlink -f $GENERATED_DOC_DIR)
if [ "$CIRCLE_BRANCH" = "master" ]
then
dir=dev
dir=docs # NOTE: I needed to change this from dev to docs for gh-pages to work
else
# Strip off .X
dir="${CIRCLE_BRANCH::-2}"

0 comments on commit 7bf34d7

Please sign in to comment.