diff options
Diffstat (limited to 'tools/gnu/classpath/tools/gjdoc/Main.java')
| -rw-r--r-- | tools/gnu/classpath/tools/gjdoc/Main.java | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/tools/gnu/classpath/tools/gjdoc/Main.java b/tools/gnu/classpath/tools/gjdoc/Main.java index feb30863d..5d9638697 100644 --- a/tools/gnu/classpath/tools/gjdoc/Main.java +++ b/tools/gnu/classpath/tools/gjdoc/Main.java @@ -1308,12 +1308,17 @@ public final class Main void process(String[] args) { option_source = args[0]; - if (!"1.2".equals(option_source) + if ("1.5".equals(option_source) + || "1.6".equals(option_source) + || "1.7".equals(option_source)) { + System.err.println("WARNING: support for option -source " + option_source + " is experimental"); + } + else if (!"1.2".equals(option_source) && !"1.3".equals(option_source) && !"1.4".equals(option_source)) { - throw new RuntimeException("Only he following values are currently" - + " supported for option -source: 1.2, 1.3, 1.4."); + throw new RuntimeException("Only the following values are currently" + + " supported for option -source: 1.2, 1.3, 1.4; experimental: 1.5, 1.6, 1.7."); } } }); |