Fix a small bug

I don't understand. I thought it was fixed in 0477d3bd83eadc49aae2585bd7b6015bca2e4d71 .