In particular, makes clearer the distinction between configuration and
configuration file. The former includes information that is not in the
latter (command-line options.)