diff options
| author | pommicket <pommicket@gmail.com> | 2025-09-23 01:54:50 -0400 |
|---|---|---|
| committer | pommicket <pommicket@gmail.com> | 2025-09-23 01:54:50 -0400 |
| commit | 6ae91130c7c2ff1c11ecfe5798d8037954a4d570 (patch) | |
| tree | 8b17b7bd02adc10c58737c96f422dddcc098a0a9 /site | |
| parent | 83ee81133b2c8a853330c8b683c391068ce36a97 (diff) | |
Stricter requirements about locations of sections
Diffstat (limited to 'site')
| -rw-r--r-- | site/spec.html | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/site/spec.html b/site/spec.html index 068d688..704395b 100644 --- a/site/spec.html +++ b/site/spec.html @@ -456,8 +456,11 @@ time = 35 min Useful for reporting invalid values. If a key <i>k</i> isn’t given a value in the configuration, but a key of the form <i>k</i><code>.</code><i>j</i> is, then the - location of the definition of an arbitrary such key - should be considered the location of <i>k</i>. + location of the definition of the earliest such key + should be considered the location of <i>k</i>. Here “earliest” means having + the least line number; when there are keys from multiple files to consider + (as may be the case in merged configurations), + which one is earliest is determined arbitrarily. </li> <li> <code>get(conf: Configuration, key: String) -> Optional<String></code><br> |