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).

Reply via email to