Rename doc/index.html to index.html #2

	name: Copy doc/main.pdf to root

	on:
	push:
	branches:
	- doc
	- main

	permissions:
	contents: write

	jobs:
	move-pdf-and-push:
	runs-on: ubuntu-latest

	steps:
	- name: Checkout repository
	uses: actions/checkout@v3

	- name: Copy PDF if exists
	run: \|
	if [ -f doc/main.pdf ]; then
	cp doc/main.pdf main.pdf
	else
	echo "doc/main.pdf does not exist, skipping move step."
	fi


	- name: Set up Git
	run: \|
	git config user.email "[email protected]"
	git config user.name "GitHub Actions"
	base_branch=$(echo "${GITHUB_REF#refs/heads/}")

	- name: Commit and push changes
	run: \|
	if git diff-index --quiet HEAD; then
	echo "No changes to commit, skipping commit and push."
	else
	git add --all
	git commit -m "Copy main.pdf to root folder"
	git push origin $base_branch
	fi

Provide feedback