Skip to content

Merge pull request #72 from OleksandrKvl:OleksandrKvl/simplify-primit… #91

Merge pull request #72 from OleksandrKvl:OleksandrKvl/simplify-primit…

Merge pull request #72 from OleksandrKvl:OleksandrKvl/simplify-primit… #91

name: Documentation workflow
permissions:
contents: write
env:
BUILD_DIR: ${{github.workspace}}/build
SELECTOR_FILE_NAME: version_selector.html
GIT_USER_NAME: 'Oleksandr Koval'
GIT_USER_EMAIL: '[email protected]'
on:
# to update docs/git-main
push:
branches:
- main
# to publish docs/<release-version>
release:
types: [released]
jobs:
publish-docs:
runs-on: ubuntu-22.04
steps:
- uses: actions/checkout@v4
- name: Install deps
shell: bash
run: |
sudo apt install -y cmake
sudo apt install -y wget
wget -nv https://www.doxygen.nl/files/doxygen-1.10.0.linux.bin.tar.gz
tar -xzf doxygen-1.10.0.linux.bin.tar.gz
echo "$(pwd)/doxygen-1.10.0/bin" >> $GITHUB_PATH
- name: CMake configure
run: cmake -DSBEPP_BUILD_SBEPPC=OFF -DSBEPP_BUILD_DOCS=ON -B $BUILD_DIR
- name: CMake build
run: cmake --build $BUILD_DIR --target doc
- name: Get docs version
id: get-docs-version
run: |
subdir=$(basename $(find $BUILD_DIR/doc/docs -mindepth 1 -maxdepth 1 -type d | head -n 1))
echo "version=$subdir" >> $GITHUB_OUTPUT
- name: Update redirect HTML
if: github.event_name == 'release'
run: |
mkdir $BUILD_DIR/doc/docs/redirect
cat << EOF > $BUILD_DIR/doc/docs/redirect/index.html
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<meta http-equiv="refresh" content="0; url=${{ steps.get-docs-version.outputs.version }}/index.html">
<title>Redirecting...</title>
</head>
<body>
<p>If you are not redirected automatically, <a href="${{ steps.get-docs-version.outputs.version }}/index.html">click here</a>.</p>
</body>
</html>
EOF
- name: Deploy release docs
if: github.event_name == 'release'
uses: peaceiris/actions-gh-pages@v4
with:
github_token: ${{ secrets.GITHUB_TOKEN }}
publish_dir: ${{ env.BUILD_DIR }}/doc/docs/${{ steps.get-docs-version.outputs.version }}
destination_dir: ${{ steps.get-docs-version.outputs.version }}
- name: Deploy redirect page
if: github.event_name == 'release'
uses: peaceiris/actions-gh-pages@v4
with:
github_token: ${{ secrets.GITHUB_TOKEN }}
publish_dir: ${{ env.BUILD_DIR }}/doc/docs/redirect
keep_files: true
- name: Deploy git-main docs
if: github.event_name == 'push'
uses: peaceiris/actions-gh-pages@v4
with:
github_token: ${{ secrets.GITHUB_TOKEN }}
publish_dir: ${{ env.BUILD_DIR }}/doc/docs/${{ steps.get-docs-version.outputs.version }}
destination_dir: git-main
# Update version_selector.html
- name: Pull gh-pages
uses: actions/checkout@v4
with:
ref: gh-pages
- name: Discover versions
run: |
# Enumerate directories and store them in a variable
dirs=$(find . -mindepth 1 -maxdepth 1 -type d | sort -rV)
# Create HTML
echo '<select id="versionSelector">' > $SELECTOR_FILE_NAME
for dir in $dirs; do
if [[ "$(basename "$dir")" != .* ]]; then
version=$(basename "$dir")
echo " <option value=\"$version\">$version</option>" >> $SELECTOR_FILE_NAME
fi
done
echo '</select>' >> $SELECTOR_FILE_NAME
- name: Push selector
run: |
git config --global user.name $GIT_USER_NAME
git config --global user.email $GIT_USER_EMAIL
if [[ -n "$(git diff --exit-code $SELECTOR_FILE_NAME)" ]]; then
git add $SELECTOR_FILE_NAME
git commit -m "Update version selector"
git push origin gh-pages
else
echo "$SELECTOR_FILE_NAME has not been changed. Skipping push."
fi