Merge branch 'main' into feature/btree #8

	# The objective of this GitHub Action is to update the DIRECTORY.md file (if needed)
	# when doing a git push
	name: directory_writer
	on: [push]
	jobs:
	build:
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v4
	with:
	fetch-depth: 0
	- uses: actions/setup-python@v5
	with:
	python-version: 3.x
	- name: Write DIRECTORY.md
	run: \|
	scripts/build_directory_md.py 2>&1 \| tee DIRECTORY.md
	git config --global user.name "$GITHUB_ACTOR"
	git config --global user.email "$GITHUB_ACTOR@users.noreply.github.com"
	git remote set-url origin https://x-access-token:${{ secrets.GITHUB_TOKEN }}@github.com/$GITHUB_REPOSITORY
	- name: Update DIRECTORY.md
	run: \|
	git add DIRECTORY.md
	git commit -am "updating DIRECTORY.md" \|\| true
	git push --force origin HEAD:$GITHUB_REF \|\| true

Provide feedback