diff --git a/doc/gawktexi.in b/doc/gawktexi.in
index 3b46ef7..61b29b5 100644
--- a/doc/gawktexi.in
+++ b/doc/gawktexi.in
@@ -31438,6 +31438,7 @@ BEGIN @{
     if (! adequate_math_precision(fpbits)) @{
         print("Error: insufficient computation precision available.\n" \
               "Try again with the -M argument?") > "/dev/stderr"
+        # Note: exit will jump to the @code{END} rules, if present (@pxref{Exit Statement})
         exit 1
     @}
 @}