Comment by Jakob

See https://news.ycombinator.com/item?id=23341711 if that really interests you.

Of course it doesn’t matter in in the grand scheme of things. We are talking about saving seconds in the most egregious example. But it’s nice to know one’s tools.