Overhauled GitHub Workflow for documentation generation. #7
This file contains hidden or 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
| # https://github.com/actions/starter-workflows/blob/main/pages/static.yml | |
| # https://github.com/actions/configure-pages | |
| # https://github.com/actions/checkout | |
| # https://github.com/actions/upload-pages-artifact | |
| # https://github.com/actions/deploy-pages | |
| name: Deploy to GitHub Pages | |
| on: | |
| # Runs on pushes targeting the default branch | |
| push: | |
| branches: | |
| - main | |
| # Allows you to run this workflow manually from the Actions tab | |
| workflow_dispatch: | |
| # 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 | |
| # Default to bash | |
| defaults: | |
| run: | |
| shell: bash | |
| jobs: | |
| # Single deploy job since we're just deploying | |
| deploy: | |
| environment: | |
| name: github-pages | |
| url: ${{ steps.deployment.outputs.page_url }} | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Install Essential Build Tools | |
| run: sudo apt -y install build-essential | |
| - name: Install Emacs | |
| run: sudo apt -y install emacs-nox | |
| - name: Install TeXLive | |
| run: sudo apt -y install texlive-full | |
| - name: Install LaTeX Make | |
| run: sudo apt -y install latexmk | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| with: | |
| submodules: recursive | |
| - name: Setup Pages | |
| uses: actions/configure-pages@v5 | |
| - name: Build with Emacs/Org | |
| run: make clean doc install-doc | |
| - name: Gather artifacts A | |
| run: mkdir public | |
| - name: Gather artifacts B | |
| run: cp -r doc/index.html public/ | |
| - name: Gather artifacts C | |
| run: cp -r _install/share public/ | |
| - name: Upload artifact | |
| uses: actions/upload-pages-artifact@v3 | |
| with: | |
| path: public/ | |
| - name: Deploy to GitHub Pages | |
| id: deployment | |
| uses: actions/deploy-pages@v4 |