polish this release

Some commits to polish up this release. Details in the commit message. Should be merged after !1240 (merged) since it is based on it.