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

Author: user202729

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

@@ -0,0 +1,8 @@
+#!/bin/sh
+expected_num_errors=1
+
+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 ]

.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: |