The rest looks fine, so I'll push the commits to nongnu.git.