Move generated docs to root dir

This commit is contained in:
Paweł Bylica 2018-03-28 22:17:41 +02:00
parent 36830eb700
commit 20fd4ebeb4
No known key found for this signature in database
GPG Key ID: 7A0C037434FE77EF
2 changed files with 4 additions and 4 deletions

View File

@ -140,7 +140,7 @@ IGNORE_PREFIX =
# Configuration options related to the HTML output # Configuration options related to the HTML output
#--------------------------------------------------------------------------- #---------------------------------------------------------------------------
GENERATE_HTML = YES GENERATE_HTML = YES
HTML_OUTPUT = docs HTML_OUTPUT = .
HTML_FILE_EXTENSION = .html HTML_FILE_EXTENSION = .html
HTML_HEADER = HTML_HEADER =
HTML_FOOTER = HTML_FOOTER =

View File

@ -22,7 +22,7 @@ jobs:
- run: - run:
name: "Test documentation" name: "Test documentation"
command: | command: |
doxygen docs/Doxyfile > doxygen.log 2> doxygen.warnings doxygen Doxyfile > doxygen.log 2> doxygen.warnings
if [ -s doxygen.warnings ]; then if [ -s doxygen.warnings ]; then
printf '\n\nDoxygen warnings:\n\n' printf '\n\nDoxygen warnings:\n\n'
cat doxygen.warnings cat doxygen.warnings
@ -37,13 +37,13 @@ jobs:
- checkout - checkout
- run: - run:
name: "Generate documentation" name: "Generate documentation"
command: doxygen docs/Doxyfile command: doxygen Doxyfile
- run: - run:
name: "Upload documentation" name: "Upload documentation"
command: | command: |
git config user.email "docs-bot@ethereum.org" git config user.email "docs-bot@ethereum.org"
git config user.name "Documentation Bot" git config user.name "Documentation Bot"
git add docs git add --all
git commit -m "Update docs" git commit -m "Update docs"
git push -f "https://$GITHUB_TOKEN@github.com/ethereum/evmc.git" HEAD:gh-pages git push -f "https://$GITHUB_TOKEN@github.com/ethereum/evmc.git" HEAD:gh-pages