I just checked, and I see that my documentation patches have not been pushed. Any objection to pushing them before the release? If you are willing to do that, I'd appreciate it. I prefer not to do anything irrevocable to the git repo.... Best, r