From 68c62193439ec90d34a7988c6a1a73b3e553a435 Mon Sep 17 00:00:00 2001 From: Valentin Gagarin Date: Tue, 20 Jun 2023 12:12:23 +0200 Subject: [PATCH] clarify setting options on the command line --- doc/manual/src/command-ref/conf-file-prefix.md | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/doc/manual/src/command-ref/conf-file-prefix.md b/doc/manual/src/command-ref/conf-file-prefix.md index 3cd622247..1e4085977 100644 --- a/doc/manual/src/command-ref/conf-file-prefix.md +++ b/doc/manual/src/command-ref/conf-file-prefix.md @@ -49,12 +49,22 @@ extra-substituters = c d defines the `substituters` setting to be `a b c d`. +Unknown option names are not an error, and are simply ignored with a warning. + ## Command line flags -Every configuration setting has a corresponding command line flag (e.g. `--max-jobs 16`). -Boolean settings do not need an argument, and can be explicitly disabled with the `no-` prefix (e.g. `--keep-failed` and `--no-keep-failed`). +Configuration options can be set on the command line, overriding the values set in the [configuration file](#configuration-file): -Existing settings can be appended to using the `extra-` prefix (e.g. `--extra-substituters`). +- Every configuration setting has corresponding command line flag (e.g. `--max-jobs 16`). + Boolean settings do not need an argument, and can be explicitly disabled with the `no-` prefix (e.g. `--keep-failed` and `--no-keep-failed`). + + Unknown option names are invalid flags (unless there is already a flag with that name), and are rejected with an error. + +- The flag `--option ` is interpreted exactly like a ` = ` in a setting file. + + Unknown option names are ignored with a warning. + +The `extra-` prefix is supported for settings that take a list of items (e.g. `--extra-trusted users alice` or `--option extra-trusted-users alice`). # Available settings