Merge branch 'main' into dev #11

	name: Python script to update documentations and header details on merge

	on:
	push:
	branches:
	- dev

	jobs:
	run-script:
	runs-on: ubuntu-latest

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

	- name: Set up Python
	uses: actions/setup-python@v5
	with:
	python-version: '3.x'

	- name: Install dependencies
	run: \|
	pip install -r requirements.txt \|\| true # skip if no file

	- name: Run script
	run: python auxiliary/updater.py

	- name: Commit and push changes
	if: success()
	run: \|
	git config user.name "github-actions[bot]"
	git config user.email "github-actions[bot]@users.noreply.github.com"
	git add -A
	git diff-index --quiet HEAD \|\| git commit -m "Automated update after merge"
	git push

Provide feedback