make_docs workflow: update directory listings folder #6

	name: Create documentation and push to gh-pages

	on:
	push:
	branches: [ main ]
	tags: [ 'v..*' ]
	pull_request:
	branches: [ main ]
	workflow_dispatch:

	jobs:
	make_docs:
	name: Create and push docs (${{ github.ref_name }})
	runs-on: ubuntu-latest
	steps:
	- name: Check out ${{ github.ref_name }}
	uses: actions/checkout@v4
	- name: Set up Python 3.11
	uses: actions/setup-python@v5
	with:
	python-version: '3.11'
	- name: Install packages
	run: \|
	python -m pip install . pdoc
	- name: Run pdoc
	run: \|
	pdoc fast_forward !fast_forward.examples -d google -o ./out
	- name: Push to gh-pages
	uses: peaceiris/actions-gh-pages@v3
	with:
	github_token: ${{ secrets.GITHUB_TOKEN }}
	publish_dir: ./out
	destination_dir: docs/${{ github.ref_name }}
	make_directory_listing:
	needs: make_docs
	runs-on: ubuntu-latest
	name: Create directory listings index file
	steps:
	- name: Check out gh-pages
	uses: actions/checkout@v4
	with:
	ref: gh-pages
	- name: Remove old directory listing
	run: \|
	rm -f docs/index.html
	- name: Generate directory listing
	uses: jayanta525/[email protected]
	with:
	FOLDER: .
	- name: Push to gh-pages
	uses: peaceiris/actions-gh-pages@v3
	with:
	github_token: ${{ secrets.GITHUB_TOKEN }}
	publish_dir: docs
	destination_dir: docs

Provide feedback