Skip to content

Merge branch 'tools/build-pdfs-only-when-needed' of https://github.co… #420

Merge branch 'tools/build-pdfs-only-when-needed' of https://github.co…

Merge branch 'tools/build-pdfs-only-when-needed' of https://github.co… #420

Workflow file for this run

name: Node CI
on: push
jobs:
build:
runs-on: ubuntu-latest
strategy:
matrix:
node-version: [18.x]
steps:
- uses: actions/checkout@v3
- name: Use Node.js ${{ matrix.node-version }}
uses: actions/setup-node@v3
with:
node-version: ${{ matrix.node-version }}
cache: 'npm'
- name: Setup pandoc
uses: nikeee/setup-pandoc@v1
with:
pandoc-version: 3.1.2
- name: Build docs
run: |
npm ci
npm run build
git config user.name ${GITHUB_ACTOR}
git config user.email ${PUSHER_EMAIL}
git add docs/*/*.html docs/*/*.md docs/*/styles/*
for dir in docs/*/ # list directories in the form "docs/dirname/"
do
doc=${dir%/} # remove the trailing "/"
doc=${doc##*/} # retain everything after the final "/"
git diff-index --quiet HEAD $dir/*.html $dir/*.md $dir/styles/* || npm run pdf $doc
done
git add docs/*/*.pdf
git diff-index --quiet HEAD docs/*/*.html docs/*/*.md docs/*/styles/* docs/*/*.pdf || git commit -m "auto-refreshed"
test `git branch --show-current` && git push
env:
PUSHER_EMAIL: ${{ github.event.pusher.email }}