Richard sent an off-list reply (I didn't realize it was off-list until later) saying that the above looked like a good solution. So I made the change (commit 3a3aa0e05), then reverted (commit 6d2e8fdd) after Eli reiterated that he didn't see a problem with the original code. I mistakenly thought we had consensus on the change, but clearly I was wrong and further discussion is needed.