Merge pull request #5982 from kenjis/deploy-userguide-latest-edit-this-page

chore: add "Edit this page" to the userguide latest

Author: kenjis

.github/workflows/deploy-userguide-latest.yml

@@ -21,12 +21,25 @@ jobs:
       - name: Checkout
         uses: actions/checkout@v3
 
+      - name: Setup PHP
+        uses: shivammathur/setup-php@v2
+        with:
+          php-version: '8.0'
+          coverage: none
+
       # Build the latest User Guide
       - name: Build with Sphinx
         uses: ammaraskar/sphinx-action@0.4
         with:
           docs-folder: user_guide_src/
 
+      - name: Add "Edit this page" links
+        run: |
+          cd user_guide_src
+          # Fix permissions
+          sudo chown -R runner:docker build/html/
+          php add-edit-this-page build/html/
+
       # Create an artifact of the html output
       - name: Upload artifact
         uses: actions/upload-artifact@v3

user_guide_src/add-edit-this-page

@@ -47,10 +47,10 @@ foreach ($files as $filePath => $fileInfo) {
         continue;
     }
 
-    $pattern = '/<div role="navigation" aria-label="breadcrumbs navigation">/u';
+    $pattern = '/<div class="rst-content">/u';
     $content = preg_replace(
         $pattern,
-        $gitHubLink . PHP_EOL . '<div role="navigation" aria-label="breadcrumbs navigation">',
+        '<div class="rst-content">' . PHP_EOL . $gitHubLink . PHP_EOL,
         $content
     );