Build and add wiki release #337
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
| name: Build and add wiki release | |
| # Only run when the wiki is updated | |
| on: | |
| - gollum | |
| - workflow_dispatch | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| jobs: | |
| make_pdf: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - run: sudo apt install pandoc texlive-xetex | |
| - working-directory: util/wiki | |
| run: | | |
| python3 -m venv venv | |
| venv/bin/pip3 install -r requirements.txt | |
| - run: pandoc --version | |
| - working-directory: util/wiki | |
| run: | | |
| git clone https://github.com/utwente-fmt/vercors.wiki.git | |
| venv/bin/python3 ./generate_wiki_pdf.py -i vercors.wiki --html wiki.html --pdf wiki.pdf | |
| - working-directory: util/wiki | |
| run: ls | |
| - name: Set wiki pdf tag in github repo | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| run: | | |
| git config --local user.name "Vercors Team" | |
| git config --local user.email "[email protected]" | |
| git tag --force wiki-generated-doc | |
| git remote set-url origin https://${GITHUB_TOKEN}@github.com/utwente-fmt/vercors.git | |
| git push --force --tags | |
| - name: Create Wiki PDF release | |
| uses: ncipollo/[email protected] | |
| with: | |
| allowUpdates: true | |
| artifacts: "util/wiki/wiki.pdf,util/wiki/wiki.html" | |
| artifactContentType: application/pdf | |
| body: "These are automatically generated versions of the tutorial on the VerCors wiki. There are two artefacts of interest: the Latex/PDF version, suitable for printing, and the HTML version, suitable for offline viewing." | |
| name: VerCors Wiki PDF | |
| prerelease: true | |
| tag: wiki-generated-doc | |
| token: ${{ secrets.GITHUB_TOKEN }} | |
| # instead of secrets.GITHUB_TOKEN, it should be a personal access token from the vercors-bot. So to implement: | |
| # 1. Create a personal access token from vercors bot | |
| # 2. add this to the secrets of the vercors repo | |
| # 3. Replace the GITHUB_TOKEN secret below with the vercors bot personal access token | |
| # 4. Uncomment this section. I think it should work! | |
| # - name: Trigger website update | |
| # env: | |
| # GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| # run: | | |
| # git clone https://user:[email protected]/utwente-fmt/vercors-web-build.git | |
| # cd vercors-web-build | |
| # git config --local user.name "Vercors Team" | |
| # git config --local user.email "[email protected]" | |
| # git commit --allow-empty -m "Trigger website refresh" | |
| # git push | |