Fixes #3083. I can't believe this was unfixed for so long, as it's
really a rather easy fix.