gh-39542: Hide more chronic diff on CI

    
When you click on the "changes is ready!" button posted by github-
actions, sometimes when a new code block is added/removed, a lot of
irrelevant diff is shown. This pull request fixes it.

Note: looks like the diff is against the last release, so we can't test
this until after the next release. But the change looks simple enough
that it can't have any bug… right.

### 📝 Checklist

<!-- Put an `x` in all the boxes that apply. -->

- [x] The title is concise and informative.
- [x] The description explains in detail what this PR is about.
- [ ] I have linked a relevant issue or discussion.
- [ ] I have created tests covering the changes.
- [ ] I have updated the documentation and checked the documentation
preview.

### ⌛ Dependencies

<!-- List all open PRs that this PR logically depends on. For example,
-->
<!-- - #12345: short description why this is a dependency -->
<!-- - #34567: ... -->
    
URL: #39542
Reported by: user202729
Reviewer(s): Frédéric Chapoton

.github/workflows/doc-build.yml

@@ -230,6 +230,7 @@ jobs:
                                                   -e '\;<script type="application/vnd\.jupyter\.widget-state+json">;,\;</script>; d' \
                                                   -e 's;#L[0-9]*";";' \
                                                   -e 's;tab-set--[0-9]*-;tab-set-;' \
+                                                  -e 's;"tab-set--[0-9]*";"tab-set";' \
              && git commit -a -m 'wipe-out')
             # Since HEAD is at commit 'wipe-out', HEAD~1 is commit 'new' (new doc), HEAD~2 is commit 'old' (old doc)
             (cd doc && git diff $(git rev-parse HEAD~2) -- "*.html") > diff.txt