Skip to content

Update index.md

Update index.md #729

Workflow file for this run

name: GitHub Pages
on:
push:
branches:
- 'master'
workflow_dispatch:
repository_dispatch:
types: [build_documentation]
concurrency:
group: publish_gh_pages
cancel-in-progress: true
jobs:
docs:
name: "Deploy"
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@main
- name: Dependencies
run: |
sudo apt update
sudo apt install -y python3-wheel python3-setuptools
pip install --break-system-packages --upgrade Jinja2
pip install --break-system-packages --user mkdocs
pip install --break-system-packages --user $(mkdocs get-deps)
pip install --break-system-packages --upgrade pygments
echo "${HOME}/.local/bin" >> ${GITHUB_PATH}
- name: Configure Git
run: |
git config --global push.default upstream
git config --global user.name "GitHub Actions"
git config --global user.email "[email protected]"
git remote set-url origin https://x-access-token:${{ secrets.GITHUB_TOKEN }}@github.com/${{ github.repository }}.git
- name: Build Mkdocs
run: |
mkdocs build
- name: Create and prepare gh-pages anew
run: |
git checkout --orphan gh-pages
rm -R `ls -A | grep -v -E "^(.git|site)$"`
mv site/* ./
- name: Commit and push
run: |
git add .
git commit -m "publish site"
git push --force --set-upstream origin gh-pages