Add docker cache and save disk space #2

	on:
	push:
	branches: [ "master" ]
	pull_request:
	branches: [ "master" ]
	workflow_dispatch: { }

	# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
	permissions:
	contents: "write"
	pages: "write"
	id-token: "write"

	# Allow only one concurrent deployment, skipping runs queued between the run in-progress and latest queued.
	# However, do NOT cancel in-progress runs as we want to allow these production deployments to complete.
	concurrency:
	group: "pages"
	cancel-in-progress: false

	jobs:
	build-and-deploy:

	runs-on: "ubuntu-latest"

	environment:
	name: "github-pages"
	url: "${{ steps.deployment.outputs.page_url }}"

	steps:
	# Prepare
	- uses: "actions/checkout@v4"
	with:
	lfs: "true"
	- uses: "ScribeMD/[email protected]"
	with:
	key: "docker-${{ runner.os }}-${{ hashFiles('docker/Dockerfile', 'docker/Dockerfile.c2w') }}"
	- run: \| # Save disk space to be able to build
	sudo rm -rf /usr/share/dotnet
	sudo rm -rf /opt/ghc
	sudo rm -rf "/usr/local/share/boost"
	sudo rm -rf "$AGENT_TOOLSDIRECTORY"

	# Build
	- run: "./build.sh"

	# Deploy
	- uses: "actions/configure-pages@v5"
	- uses: "actions/upload-pages-artifact@v3"
	with:
	path: 'export'
	- id: "deployment"
	uses: "actions/deploy-pages@v4"

Provide feedback