Skip to content

Merge pull request #77 from dinkelk/artifacts #385

Merge pull request #77 from dinkelk/artifacts

Merge pull request #77 from dinkelk/artifacts #385

name: Build the User Guide
on:
push:
branches:
- main
pull_request:
branches:
- main
workflow_dispatch:
jobs:
compile_job:
name: build_user_guide
runs-on: ubuntu-latest
container:
image: ghcr.io/lasp/adamant:latest
options: --user root
steps:
- run: echo "Starting job triggered by a ${{ github.event_name }} event on a ${{ runner.os }} server hosted by GitHub."
- run: echo "Checking out ${{ github.repository }} on branch ${{ github.ref }}."
- name: Check out repository code
uses: actions/checkout@v4
- name: Build the user guide
run: bash env/github_run.sh "redo doc/user_guide/build_user_guide"
- name: Archive user guide PDF
uses: actions/upload-artifact@v4
with:
name: user_guide
path: ${{ github.workspace }}/doc/user_guide/build/pdf/user_guide.pdf
if-no-files-found: error
- name: Build the architecture description document
run: bash env/github_run.sh "redo doc/architecture_description_document/build/pdf/architecture_description_document.pdf"
- name: Archive user guide PDF
uses: actions/upload-artifact@v4
with:
name: architecture_description_document
path: ${{ github.workspace }}/doc/architecture_description_document/build/pdf/architecture_description_document.pdf
if-no-files-found: error
- run: echo "Finished with status - ${{ job.status }}."