Automatic merge from submit-queue

Mention that comments keep pull-requests open

A comment in a pull-request will keep it open for another 90 days. Let's
mention that in the documentation for people who can't add labels.