treewide: Update docs and tutorial (#196) #133
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # Copyright 2020 ETH Zurich and University of Bologna. | |
| # Licensed under the Apache License, Version 2.0, see LICENSE for details. | |
| # SPDX-License-Identifier: Apache-2.0 | |
| name: publish-docs | |
| on: | |
| push: | |
| branches: [main] | |
| workflow_dispatch: | |
| jobs: | |
| deploy: | |
| name: Deploy documentation | |
| runs-on: ubuntu-22.04 | |
| container: | |
| image: ghcr.io/pulp-platform/snitch_cluster:main | |
| steps: | |
| - uses: actions/checkout@v2 | |
| # For some reason, the checkout is done by a different user, | |
| # than that deploying to Github (root, possibly due to Docker). | |
| # So we need to set the repository as a safe directory. | |
| - name: Git config safe.directory | |
| run: | | |
| git config --global --add safe.directory $GITHUB_WORKSPACE | |
| - name: Generate documentation sources | |
| run: | | |
| make doc-srcs | |
| make doxygen-docs | |
| - name: Build and deploy documentation | |
| run: mkdocs gh-deploy --force |