Proper highlighting of "\d*<<<" redirection.

This feature seems not mentioned in the Bash Manual.
Please attach a link to documentation about it to this bug report if you know any.