On Dec 20, 2011, at 12:23 AM, Roland McGrath wrote: > ping? Just a cosmetic comment from my part. I think it would be better to display only '(default)', and not to display '(not default)'. After all, a command line option is an option, which by default is not default :-) Otherwise, looks sane to me. Tristan.