diff options
| author |  Googler <noreply@google.com> | 2017-06-02 17:48:48 -0400 |
|---|---|---|
| committer |  John Cater <jcater@google.com> | 2017-06-05 10:19:07 -0400 |
| commit | 2db54114e0b3ed90c2ad99fc02348ee9898edbbb (patch) | |
| tree | 14724875e9b9d728190a80ee6eef76250499ceb9 /src/main/java/com/google/devtools | |
| parent | f19fcfebb81759a5ab4fe6bede35195287f89872 (diff) | |
Internal change
PiperOrigin-RevId: 157878648
Diffstat (limited to 'src/main/java/com/google/devtools')
| -rw-r--r-- | src/main/java/com/google/devtools/common/options/Converters.java | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/main/java/com/google/devtools/common/options/Converters.java b/src/main/java/com/google/devtools/common/options/Converters.java index 0d1902933a..4584f80bc2 100644 --- a/src/main/java/com/google/devtools/common/options/Converters.java +++ b/src/main/java/com/google/devtools/common/options/Converters.java @@ -459,4 +459,13 @@ public final class Converters { } } + /** + * A converter to check whether an integer denoting a percentage is in a valid range: [0, 100]. + */ + public static class PercentageConverter extends RangeConverter { + public PercentageConverter() { + super(0, 100); + } + } + } |