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

	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

Provide feedback