Skip to content

[#12679] Copying feedback session: Name for copied session should not be whitespace #5356

[#12679] Copying feedback session: Name for copied session should not be whitespace

[#12679] Copying feedback session: Name for copied session should not be whitespace #5356

Workflow file for this run

name: Build Developer Guide
on:
push:
branches:
- master
pull_request:
branches:
- master
jobs:
build:
runs-on: ubuntu-latest
name: Dev docs
defaults:
run:
shell: bash
working-directory: docs
steps:
- uses: actions/checkout@v4
- uses: actions/setup-node@v4
with:
node-version: 18
- uses: actions/setup-java@v4
with:
java-version: 11
distribution: temurin
- name: Install Graphviz
run: sudo apt install graphviz
- run: npm ci
- run: npm run build
- name: Check build status
run: |
if [ ! -d "./_site" ]; then
echo "Build Error"
exit 1
fi
- name: Deploy on push
if: ${{ success() && github.event_name == 'push' }}
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
run: npm run deploy