diff --git a/.github/workflows/users-guide.yml b/.github/workflows/users-guide.yml new file mode 100644 index 00000000000..3f75d5d24d7 --- /dev/null +++ b/.github/workflows/users-guide.yml @@ -0,0 +1,61 @@ +# Adapted from agda/agda/.github/workflows/user-manual.yml by Andreas, 2021-09-11 + +name: Users guide + +on: + push: + branches: + - master + paths: + - 'doc/requirements.txt' + - 'doc/*.inc' + - 'doc/*.py' + - 'doc/*.rst' + - 'doc/**/*.json' + - '.github/workflows/users-guide.yml' + pull_request: + paths: + - 'doc/requirements.txt' + - 'doc/*.inc' + - 'doc/*.py' + - 'doc/*.rst' + - 'doc/**/*.json' + - '.github/workflows/users-guide.yml' + release: + types: + - created + +jobs: + build: + if: | + !contains(github.event.head_commit.message, '[skip ci]') + && !contains(github.event.head_commit.message, '[ci skip]') + + runs-on: ubuntu-latest + strategy: + matrix: + python-version: [3.7] + + steps: + - uses: actions/checkout@v2 + with: + submodules: recursive + + - name: Set up Python ${{ matrix.python-version }} + uses: actions/setup-python@v2 + with: + python-version: ${{ matrix.python-version }} + + # Subsumed by make users-guide + # - name: Install dependencies + # run: | + # pip install -r doc/requirements.txt + + - name: Build User's Guide in HTML + run: | + make SPHINX_HTML_OUTDIR=html users-guide + + - uses: actions/upload-artifact@v2 + with: + name: users-guide-html + path: html/