-
Vladimír Čunát authored
It's about a hundred of them. The price is making two printf calls instead of one. That seems acceptable; these warning tools can help us in future, and the likelihood of mixing outputs from different processes seems relatively small.