Oops, I forgot to say explicitly: this is okay to merge.