diff options
author | 2017-10-16 22:18:32 +0200 | |
---|---|---|
committer | 2017-10-18 10:27:58 +0200 | |
commit | 7cd9e883dd31f54cd505844aa1f1e0ed7bd9f380 (patch) | |
tree | e72e67a2f22108d490aaf4b5a59e5727e855547d /src/main/java/com/google/devtools/skylark | |
parent | b6bf11217c30123827d36a35a3614ba8e200f349 (diff) |
Track Option placement within a priority category.
An option has precedence over previous options at the same enum-valued priority. Track its placement in this ordering explicitly.
This will allow after-the-fact expansion of expansion options such that they correctly take precedence or not compared to other mentions of the same flag. This is needed to fix --config's expansion.
RELNOTES: None.
PiperOrigin-RevId: 172367996
Diffstat (limited to 'src/main/java/com/google/devtools/skylark')
0 files changed, 0 insertions, 0 deletions