Retouch my last change after a comment on style from Guido.
1 file changed