> So ok, unless someone else thinks otherwise, that's the decision :). I have just adopted fmtutil.in for that (#4841). We can change that at any time if we decide so... Thomas