Merge pull request #1348 from pguyot/w43/fix-docs-path

Fix docs build when branch names contain a /

These changes are made under both the "Apache 2.0" and the "GNU Lesser General
Public License 2.1 or later" license terms (dual license).

SPDX-License-Identifier: Apache-2.0 OR LGPL-2.1-or-later

.github/workflows/build-docs.yaml

@@ -95,9 +95,9 @@ jobs:
         shell: bash
         run: |
             if [[ ${{ github.ref_name }} == *"/merge" ]]; then
-              echo "AVM_DOCS_NAME=${{github.event.pull_request.base.ref}}" >> "$GITHUB_ENV";
+              echo "AVM_DOCS_NAME=${{ github.event.pull_request.base.ref }}" | tr '/' '-' >> "$GITHUB_ENV";
             else
-              echo "AVM_DOCS_NAME=${{ github.ref_name }}" >> "$GITHUB_ENV";
+              echo "AVM_DOCS_NAME=${{ github.ref_name }}" | tr '/' '-' >> "$GITHUB_ENV";
             fi
 
       - uses: actions/checkout@v4