/*
 * miniprintf works like printf, except that it only
 * understands the '%d' identifier.
 *
 * No other cases need to be handled.
 */