Browse Source

build: Don't build documentation before pushing

Ole 9 years ago
parent
commit
25cd41f6b0
1 changed files with 1 additions and 1 deletions
  1. 1 1
      Makefile

+ 1 - 1
Makefile

@@ -39,7 +39,7 @@ docs:
 	mkdocs build --clean
 	mkdocs build --clean
 	doxygen
 	doxygen
 
 
-push-gh-pages: docs
+push-gh-pages:
 	git subtree push --prefix docs/output origin gh-pages
 	git subtree push --prefix docs/output origin gh-pages
 
 
 # Tests
 # Tests