void print_version(FILE *);