Allow multiple same jsr305 options in the command-line

do not report duplicate jsr305 entries if options are the same
2018-07-05 13:37:45 +02:00
parent 563e4c9e57
commit ec58929e39
3 changed files with 12 additions and 8 deletions
@@ -6,7 +6,9 @@ $TEMP_DIR$
 -Xjsr305=@hello\:warning
 -Xjsr305=@hello\:warn
 -Xjsr305=@hello\:ignore
+-Xjsr305=@hello\:warn
 -Xjsr305=strict
 -Xjsr305=ignore
 -Xjsr305=under-migration\:ignore
 -Xjsr305=under-migration\:strict
+-Xjsr305=under-migration\:ignore