cc3259f8d9
Regression fromd6ad41dcea(for #732). Probably also meanseab6e9ea4ewas unnecessary, but it's fine. Fixes #887