Fix a bad argument to printf().

The ".*" max-length specifier for a printf field expects the
corresponding argument to be an int.  I was passing a size_t instead,
because it was the difference of two pointers.  Fix that.