Skip to content

Merge branch 'fix-kata' into 'master' #85

Merge branch 'fix-kata' into 'master'

Merge branch 'fix-kata' into 'master' #85

Workflow file for this run

name: docs-build
on:
pull_request:
branches: [ master ]
types: [ opened, synchronize ]
push:
branches: [ master ]
tags:
- v*
workflow_dispatch:
env:
REGISTRY: ghcr.io
IMAGE_NAME: ${{ github.repository }}
TAG: 0.1.0
concurrency:
group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
cancel-in-progress: true
jobs:
dockerfile-changed:
runs-on: ubuntu-latest
permissions:
contents: read
outputs:
changed: ${{ steps.change.outputs.changed }}
image: ${{ steps.change.outputs.image }}
steps:
- name: Checkout
uses: actions/checkout@v3
with:
fetch-depth: 2
- name: Detect change
id: change
run: |
first_commit=$(git rev-list HEAD | tail -n 1)
diff=$(git diff --name-only HEAD..${first_commit})
if [[ "${diff}" =~ docker/Dockerfile ]] && [[ "${{ github.event_name }}" == 'pull_request' ]]; then
echo "changed=true" >> "$GITHUB_OUTPUT"
echo "image=${REGISTRY}/${IMAGE_NAME}:${{ github.event.pull_request.number }}" >> "$GITHUB_OUTPUT"
else
echo "changed=false" >> "$GITHUB_OUTPUT"
echo "image=${REGISTRY}/${IMAGE_NAME}:${TAG}" >> "$GITHUB_OUTPUT"
fi
shell: bash
build-and-push-image:
needs: dockerfile-changed
if: needs.dockerfile-changed.outputs.changed == 'true'
runs-on: ubuntu-latest
permissions:
contents: read
packages: write
steps:
- name: Checkout
uses: actions/checkout@v3
with:
fetch-depth: 1
- name: Log in to Container Registry
uses: docker/login-action@v2
with:
registry: ${{ env.REGISTRY }}
username: ${{ github.actor }}
password: ${{ secrets.GITHUB_TOKEN }}
- name: Build and push
uses: docker/build-push-action@v4
with:
context: .
file: docker/Dockerfile
push: true
tags: ${{ needs.dockerfile-changed.outputs.image }}
build-docs:
needs: [dockerfile-changed, build-and-push-image]
if: ${{ always() }}
runs-on: ubuntu-latest
container:
image: ${{ needs.dockerfile-changed.outputs.image }}
steps:
- name: Checkout
uses: actions/checkout@v3
with:
fetch-depth: 1
- name: Set ownership
run: |
chown -R $(id -u):$(id -g) $PWD
- name: Build docs
run: |
make html
- name: Delete unnecessary files
run: |
find _build/html -name .doctrees -prune -exec rm -rf {} \;
find _build/html -name .buildinfo -exec rm {} \;
- name: Upload HTML
uses: actions/upload-artifact@v3
with:
name: html-build-artifact
path: _build/html
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@v3
with:
name: pr
path: pr/
store-html:
needs: [ build-docs ]
if: ${{ github.event_name == 'push' }}
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v3
with:
ref: "gh-pages"
- name: Initialize Git configuration
run: |
git config user.name docs-build
git config user.email do-not-send@github.com
- name: Download artifacts
uses: actions/download-artifact@v3
with:
name: html-build-artifact
- name: Copy HTML directories
run: |
ls -asl
for i in `ls -d *`
do
echo "Git adding ${i}"
git add "${i}"
done
- 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.
def_branch=$(gh api "repos/${GITHUB_REPOSITORY}" --jq ".default_branch")
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}${def_branch}'/index.html">' >> index.html
echo ' <link rel="canonical" href="'${html_url}${def_branch}'/index.html">' >> index.html
echo ' <script language="javascript">' >> index.html
echo ' function redirect() {' >> index.html
echo ' window.location.assign("'${html_url}${def_branch}'/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}${def_branch}'/index.html">' >> index.html
echo ${def_branch}'</a> branch 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