Fix document publishing GitHub Action

mermaid-filter depends on a deprecated version of puppeteer, which
results in puppeteer no longer finding a suitable version of Chromium.
See puppeteer/puppeteer#9533 for others facing
this issue. Forcing npm to use the most recent release of puppeteer
(version 21) resolves this problem.

We should revert the workflow to one that doesn't text-insert a
dependency and just directly npm installs mermaid-filter once
mermaid-js/mermaid-cli#627 has been resolved,
a new release of mermaid-cli been produced, and mermaid-filter having
picked up that new release.

.github/workflows/publish.yaml

@@ -20,7 +20,14 @@ jobs:
         run: sudo python3 -m pip install gitpython pandocfilters
 
       - name: Install mermaid diagram filter
-        run: sudo npm install --global mermaid-filter
+        run: |
+          git clone https://github.com/raghur/mermaid-filter/
+          cd mermaid-filter
+          sed -i '1s/{/{ "overrides": { "puppeteer": "^21" },/' package.json
+          sed -i '1s/^\/\/ //' index.js
+          npm install --loglevel verbose
+          sudo npm link --loglevel verbose
+          cd ..
 
       - name: Build documentation
         run: cd doc/doxygen-root && make && touch html/.nojekyll