Add a step to doc-build-pdf to check for missing character errors

.github/workflows/check-latex-build.sh

@@ -0,0 +1,9 @@
+#!/bin/sh
+expected_num_errors=36
+
+cd builddir/src/doc/latex
+echo "All missing character error messages in LaTeX log files:"
+num_errors=$(grep -r "Missing character" --include "*.log" | tee /dev/stderr | wc -l)
+echo "In total there are $num_errors missing character errors, expecting $expected_num_errors"
+[ $num_errors = $expected_num_errors ] || echo "::error title=Missing character errors introduced in PDF build::In total there are $num_errors missing character errors, expecting $expected_num_errors"
+[ $num_errors = $expected_num_errors ]

.github/workflows/doc-build-pdf.yml

@@ -80,6 +80,9 @@ jobs:
         env:
           SAGE_DOCBUILD_OPTS: "--include-tests-blocks"
 
+      - name: Check for missing character error messages
+        run: sh .github/workflows/check-latex-build.sh
+
       - name: Copy doc
         id: copy
         run: |