Change the way dim and spacedim work. #238

	name: Indent

	on: [push, pull_request]

	concurrency:
	group: ${ {github.event_name }}-${{ github.workflow }}-${{ github.ref }}
	cancel-in-progress: ${{github.event_name == 'pull_request'}}

	permissions:
	contents: read

	jobs:
	indent:
	# run the indent checks

	name: indent
	runs-on: [ubuntu-20.04]
	container:
	image: heltai/dealii:vscode
	options: --user root

	steps:
	- uses: actions/checkout@v3
	with:
	fetch-depth: 100
	- name: Check indentation
	run: \|
	git config --global --add safe.directory "$GITHUB_WORKSPACE"
	./scripts/check_indentation.sh

Provide feedback