copy release notes

This commit is contained in:
2026-01-13 12:29:33 +01:00
parent f9d96bd520
commit 4e320f4b4b

View File

@@ -38,16 +38,10 @@ jobs:
id: version id: version
run: | run: |
if [ "${{ github.event_name }}" == "release" ]; then if [ "${{ github.event_name }}" == "release" ]; then
# Remove 'v' prefix if present (e.g., v10.0.0 -> 10.0.0)
VERSION="${{ github.event.release.tag_name }}" VERSION="${{ github.event.release.tag_name }}"
VERSION="${VERSION#v}"
echo "version=${VERSION}" >> $GITHUB_OUTPUT echo "version=${VERSION}" >> $GITHUB_OUTPUT
echo "is_release=true" >> $GITHUB_OUTPUT
echo "Release version: ${VERSION}"
else else
echo "version=developer" >> $GITHUB_OUTPUT echo "version=developer" >> $GITHUB_OUTPUT
echo "is_release=false" >> $GITHUB_OUTPUT
echo "Not a release build"
fi fi
- name: Install System Packages - name: Install System Packages
@@ -74,7 +68,7 @@ jobs:
make -j4 make -j4
make docs make docs
# Update main_index if this is a release # Update main index if this is a release
- name: Update version index - name: Update version index
run: | run: |
if [ "${{ github.event_name }}" == "release" ]; then if [ "${{ github.event_name }}" == "release" ]; then
@@ -89,12 +83,16 @@ jobs:
ref: gh-pages ref: gh-pages
path: gh-pages path: gh-pages
- name: Copy documentation to versioned folder - name: Copy documentation and Release notes to versioned folder
run: | run: |
VERSION="${{ steps.version.outputs.version }}" VERSION="${{ steps.version.outputs.version }}"
mkdir -p "gh-pages/${VERSION}" mkdir -p "gh-pages/${VERSION}"
cp -r build/docs/html/. "gh-pages/${VERSION}/" cp -r build/docs/html/. "gh-pages/${VERSION}/"
cp build/docs/main_index/index.html "gh-pages/index.html" cp build/docs/main_index/index.html "gh-pages/index.html"
if [ "${{ github.event_name }}" == "release" ]; then
cp RELEASE.md "gh-pages/releases/RELEASE_v${VERSION}.md"
fi
# TODO: need to update txt to md and backtrack?
- name: Commit and Push changes to gh-pages - name: Commit and Push changes to gh-pages
run: | run: |