Skip to content

Readme: Fix broken links in top level readme #14

Readme: Fix broken links in top level readme

Readme: Fix broken links in top level readme #14

Workflow file for this run

name: docs-build
on:
pull_request:
branches: [ main, release-* ]
types: [ opened, synchronize ]
push:
branches: [ main ]
tags:
- v*
workflow_dispatch:
concurrency:
group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
cancel-in-progress: true
defaults:
run:
shell: bash
jobs:
build-docs:
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v4
- name: Build image
run: |
docker build --pull --tag docs-builder:latest --file docs/Dockerfile .
- name: Build docs
run: |
docker run -v $(pwd):/work -w /work docs-builder:latest sphinx-build -b html -d /tmp docs docs/_build/output
- name: Delete unnecessary files
run: |
sudo rm -rf docs/_build/jupyter_execute
sudo rm -rf docs/_build/.buildinfo
- name: Upload HTML
uses: actions/upload-artifact@v4
with:
name: html-build-artifact
path: docs/_build/
if-no-files-found: error
retention-days: 1
- name: Store PR information
if: ${{ github.event_name == 'pull_request' }}
run: |
mkdir ./pr
echo ${{ github.event.number }} > ./pr/pr.txt
echo ${{ github.event.pull_request.merged }} > ./pr/merged.txt
echo ${{ github.event.action }} > ./pr/action.txt
- name: Upload PR information
if: ${{ github.event_name == 'pull_request' }}
uses: actions/upload-artifact@v4
with:
name: pr
path: pr/
store-html:
needs: [ build-docs ]
if: ${{ github.event_name == 'push' }}
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
with:
ref: "gh-pages"
- name: Initialize Git configuration
run: |
git config user.name docs-build
git config user.email [email protected]
- name: Download artifacts
uses: actions/download-artifact@v4
with:
name: html-build-artifact
- name: Copy HTML directories
run: |
ls -asl
- name: Store bleeding edge docs from main
if: ${{ github.ref == 'refs/heads/main' }}
run: |
mkdir main || true
rsync -av --progress --delete output/ main/
git add main
- name: Store docs for a release tag
if: ${{ startsWith(github.ref, 'refs/tags/v') }}
env:
LATEST: ${{ contains(github.event.head_commit.message, '/not-latest') && 'not-true' || 'true' }}
run: |
printenv LATEST
if [[ "${GITHUB_REF}" =~ "-rc" ]]; then
echo "Not saving documents for release candidates."
exit 0
fi
if [[ "${GITHUB_REF}" =~ v([0-9]+\.[0-9]+\.[0-9]+) ]]; then
TAG="${BASH_REMATCH[1]}"
mkdir "${TAG}" || true
rsync -av --progress --delete output/ "${TAG}/"
git add "${TAG}/"
if [[ "${LATEST}" == 'true' ]]; then
mkdir latest || true
rsync -av --progress --delete output/ latest/
cp output/versions.json .
git add latest
git add versions.json
fi
fi
- name: Check or create dot-no-jekyll file
run: |
if [ -f ".nojekyll" ]; then
echo "The dot-no-jekyll file already exists."
exit 0
fi
touch .nojekyll
git add .nojekyll
- name: Check or create redirect page
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
run: |
resp=$(grep 'http-equiv="refresh"' index.html 2>/dev/null) || true
if [ -n "${resp}" ]; then
echo "The redirect file already exists."
exit 0
fi
# If any of these commands fail, fail the build.
html_url=$(gh api "repos/${GITHUB_REPOSITORY}/pages" --jq ".html_url")
# Beware ugly quotation mark avoidance in the foll lines.
echo '<!DOCTYPE html>' > index.html
echo '<html>' >> index.html
echo ' <head>' >> index.html
echo ' <title>Redirect to documentation</title>' >> index.html
echo ' <meta charset="utf-8">' >> index.html
echo ' <meta http=equiv="refresh" content="3; URL='${html_url}'/latest/index.html">' >> index.html
echo ' <link rel="canonical" href="'${html_url}'/latest/index.html">' >> index.html
echo ' <script language="javascript">' >> index.html
echo ' function redirect() {' >> index.html
echo ' window.location.assign("'${html_url}'/latest/index.html")' >> index.html
echo ' }' >> index.html
echo ' </script>' >> index.html
echo ' </head>' >> index.html
echo ' <body onload="redirect()">' >> index.html
echo ' <p>Please follow the link to the <a href="'${html_url}'/latest/index.html">' >> index.html
echo 'latest</a> documentation.</p>' >> index.html
echo ' </body>' >> index.html
echo '</html>' >> index.html
git add index.html
- name: Commit changes to the GitHub Pages branch
run: |
git status
if git commit -m 'Pushing changes to GitHub Pages.'; then
git push -f
else
echo "Nothing changed."
fi