/* Names are passed as separate arguments, with an additional
NULL argument at the end. */
extern void version_etc (FILE *stream,
/* Names are passed as separate arguments, with an additional
NULL argument at the end. */
extern void version_etc (FILE *stream,