In the last example of this section, the web version of the book shows an error beginning with
❌️ Docstring on #guard_msgs does not match generated message:
This does not appear to be intended, since the problem is just that the Docstring has the error before the warning, but the current version of Lean outputs them in the opposite order. This is since at least August 14th 2025, when I read this part and experimented with an updated version of Lean.