equal
deleted
inserted
replaced
55 void TaskQueueStats::print_header(unsigned int line, outputStream* const stream, |
55 void TaskQueueStats::print_header(unsigned int line, outputStream* const stream, |
56 unsigned int width) |
56 unsigned int width) |
57 { |
57 { |
58 // Use a width w: 1 <= w <= max_width |
58 // Use a width w: 1 <= w <= max_width |
59 const unsigned int max_width = 40; |
59 const unsigned int max_width = 40; |
60 const unsigned int w = MAX2(MIN2(width, max_width), 1U); |
60 const unsigned int w = clamp(width, 1u, max_width); |
61 |
61 |
62 if (line == 0) { // spaces equal in width to the header |
62 if (line == 0) { // spaces equal in width to the header |
63 const unsigned int hdr_width = w * last_stat_id + last_stat_id - 1; |
63 const unsigned int hdr_width = w * last_stat_id + last_stat_id - 1; |
64 stream->print("%*s", hdr_width, " "); |
64 stream->print("%*s", hdr_width, " "); |
65 } else if (line == 1) { // labels |
65 } else if (line == 1) { // labels |