Modify github actions script for publishing documentation

- Automatically publishing users documentation on develop or main (dev/main folder)
- Automatically publishing users documentation on tag push (but including only major version number: e.g. v0)

Author: krashish8

.github/workflows/publish-users-doc.yml

@@ -2,6 +2,14 @@ name: Publish Users Documentation
 
 on:
   workflow_dispatch:
+  push:
+    branches:
+      - main
+      - develop
+    paths:
+      - 'doc/**'
+      - 'docqueries/**'
+      - 'locale/**'
 
 
 jobs:
@@ -28,6 +36,14 @@ jobs:
           echo "PGIS=3" >> $GITHUB_ENV
           echo "PROJECT_VERSION=${PROJECT_VERSION}" >> $GITHUB_ENV
 
+      - name: Extract branch name and commit hash
+        run: |
+          raw=$(git branch -r --contains ${{ github.ref }})
+          branch=${raw##*/}
+          echo "BRANCH=$branch" >> $GITHUB_ENV
+          git_hash=$(git rev-parse --short "$GITHUB_SHA")
+          echo "GIT_HASH=$git_hash" >> $GITHUB_ENV
+
       - name: Add PostgreSQL APT repository
         run: |
           sudo apt-get install curl ca-certificates gnupg
@@ -77,17 +93,20 @@ jobs:
 
       - name: Update Users Documentation
         run: |
+          if [[ "${{ env.BRANCH }}" == "main" ]]; then
+            FOLDER_NAME="main"
+          elif [[ "${{ env.BRANCH }}" == "develop" ]]; then
+            FOLDER_NAME="dev"
+          fi
           git checkout origin/gh-pages
           git checkout -b gh-pages
-          PROJECT_MAJOR_MINOR="v${PROJECT_VERSION%.*}"
-          rm -rf ${PROJECT_MAJOR_MINOR}
-          cp -r build/doc/html ${PROJECT_MAJOR_MINOR}
-          rm -rf ${PROJECT_MAJOR_MINOR}/es
-          git add ${PROJECT_MAJOR_MINOR}
-          git diff-index --quiet HEAD || git commit -m "Update users documentation for ${PROJECT_VERSION}"
+          rm -rf ${FOLDER_NAME}
+          cp -r build/doc/html ${FOLDER_NAME}
+          git add ${FOLDER_NAME}
+          git diff-index --quiet HEAD || git commit -m "Update users documentation for ${PROJECT_VERSION} (${{ env.BRANCH }}): commit ${{ env.GIT_HASH }}"
           git fetch origin
           git rebase origin/gh-pages
           git push origin gh-pages
 
         env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

.github/workflows/release.yml

@@ -99,12 +99,11 @@ jobs:
         run: |
           git checkout origin/gh-pages
           git checkout -b gh-pages
-          PROJECT_MAJOR_MINOR="v${PROJECT_VERSION%.*}"
-          rm -rf ${PROJECT_MAJOR_MINOR}
-          cp -r build/doc/html ${PROJECT_MAJOR_MINOR}
-          rm -rf ${PROJECT_MAJOR_MINOR}/es
-          git add ${PROJECT_MAJOR_MINOR}
-          git diff-index --quiet HEAD || git commit -m "Update users documentation for ${PROJECT_VERSION}"
+          PROJECT_MAJOR="v${PROJECT_VERSION%%.*}"
+          rm -rf ${PROJECT_MAJOR}
+          cp -r build/doc/html ${PROJECT_MAJOR}
+          git add ${PROJECT_MAJOR}
+          git diff-index --quiet HEAD || git commit -m "Update users documentation for ${PROJECT_VERSION} (tag ${TAG_NAME})"
           git fetch origin
           git rebase origin/gh-pages
           git push origin gh-pages
@@ -117,7 +116,7 @@ jobs:
           rm -rf doxy/main
           cp -r build/doxygen/html doxy/main
           git add doxy/main
-          git diff-index --quiet HEAD || git commit -m "Update developers documentation for ${PROJECT_VERSION}"
+          git diff-index --quiet HEAD || git commit -m "Update developers documentation for ${PROJECT_VERSION} (tag ${TAG_NAME})"
           git fetch origin
           git rebase origin/gh-pages
           git push origin gh-pages
@@ -166,4 +165,4 @@ jobs:
             ${{ github.event.repository.name }}-${{ env.PROJECT_VERSION }}.tar.gz
 
         env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}