[PATCH 0/8] trivia

Tom Tromey
2013-11-26T21:50:58Z

I have a few trivial changes I've accumulated over the years that I
never got around to submitting. I've collected them all in this
series.