Both doc patches pushed, thanks. I had to manually edit them because they wouldn't apply cleanly. Next time, please use git-send-email (see https://git-send-email.io/ for setup instructions).