diff --git a/.github/workflows/generate_doc.yml b/.github/workflows/generate_doc.yml index f76cd0a5a..cda60d97e 100644 --- a/.github/workflows/generate_doc.yml +++ b/.github/workflows/generate_doc.yml @@ -18,6 +18,13 @@ jobs: with: python-version: "3.x" + + - name: Differentiate main from tag + run: | + if [ "${{ github.ref_name }}" != "main" ] ; then + echo "new_tag=1" >> "$GITHUB_ENV" + fi + - name: Install pip packages working-directory: docs run: | @@ -33,6 +40,7 @@ jobs: working-directory: docs run: | python3 extract_macros.py ../ user_guide/preferences_table.rst + ADOC_DOC_VERSION=${{ github.ref_name }} make html SPHINXOPTS='-W --keep-going' - name: Store the generated doc @@ -44,7 +52,6 @@ jobs: deploy-doc: runs-on: ubuntu-latest needs: build-doc - if: startsWith(github.ref, 'refs/tags/') steps: - run: | @@ -58,34 +65,45 @@ jobs: ( git reset --hard ; git clean -fdx ; + git fetch origin gh-pages ; + git checkout -b gh-pages origin/gh-pages ; + DOC_BUILDS=$(find . -mindepth 2 -name objects.inv -exec sh -c 'dirname {}' ';') ; + git rm -r . --quiet || true ; + printf "Detected doc builds: $DOC_BUILDS" ; + if ! [ -z "$DOC_BUILDS" ]; then + git checkout @ -- $DOC_BUILDS ; + fi ; + if [[ "$new_tag" == "1" ]]; then + git rm -r ${{ github.ref_name }} --quiet || true ; + fi ; + ) || ( git checkout --orphan gh-pages ; - git reset --hard; - git commit -m "empty" --allow-empty ; - git push origin gh-pages:gh-pages + git reset --hard ; + git commit -m "initial commit" --allow-empty ) - - uses: actions/checkout@v4 + - uses: actions/download-artifact@v4 with: - ref: 'gh-pages' - - - name: Empty gh-pages - run: | - git rm -r . --quiet || true + name: html - uses: actions/download-artifact@v4 + if: ${{ env.new_tag == '1' }} with: - name: html + name: html-tagged + path: ${{ github.ref_name }} - - name: Patch doc build + - name: Generate aux files run: | - rm -r _sources - touch .nojekyll + touch .nojekyll ; + find . -name objects.inv -exec sh -c 'dirname {}' ';' | + cut -c 3- | sort -r | + jq --raw-input . | + jq --slurp . > tags.json - - name: Commit gh-pages + - name: Commit and push to gh-pages run: | + git config --global user.name "${{ github.event.head_commit.committer.name }}" + git config --global user.email "${{ github.event.head_commit.committer.email }}" git add . >> /dev/null git commit -m "deploy: ${GITHUB_SHA}" --allow-empty - - - name: Push to gh-pages - run: | - git push origin gh-pages:gh-pages \ No newline at end of file + git push origin gh-pages:gh-pages