# This is a basic workflow to help you get started with Actions name: Github Pages # Controls when the workflow will run on: # Triggers the workflow on push or pull request events but only for the "master" branch push: branches: [ "master" ] paths-ignore: - '.github/workflows/CI.yml' - 'doc/**' - Dockerfile - docker-compose.yml - check_features.py - README.md # Allows you to run this workflow manually from the Actions tab workflow_dispatch: env: CARGO_TERM_COLOR: always # Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages permissions: contents: read pages: write id-token: write # Allow one concurrent deployment concurrency: group: "pages" cancel-in-progress: false # A workflow run is made up of one or more jobs that can run sequentially or in parallel jobs: deploy: # The type of runner that the job will run on runs-on: ubuntu-latest environment: name: github-pages url: ${{ steps.deployment.outputs.page_url }} # Steps represent a sequence of tasks that will be executed as part of the job steps: # Checks-out your repository under $GITHUB_WORKSPACE, so your job can access it - name: Check out uses: actions/checkout@v4 with: fetch-depth: 0 submodules: true - name: Document run: | cargo doc -vv || exit 1 - name: Add index files run: | echo '
Content Moved' > target/doc/index.html - name: Setup Pages uses: actions/configure-pages@v5 - name: Upload documents uses: actions/upload-pages-artifact@v3 with: path: target/doc - name: Deploy to GitHub Pages id: deployment uses: actions/deploy-pages@v4