diff options
Diffstat (limited to 'scripts')
| -rwxr-xr-x | scripts/run-dialyzer | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/scripts/run-dialyzer b/scripts/run-dialyzer index 44436594d3..34724a8ca0 100755 --- a/scripts/run-dialyzer +++ b/scripts/run-dialyzer @@ -43,5 +43,5 @@ $ERL_TOP/bin/dialyzer --build_plt -Wunknown --apps $BASE_PLT $APP_PLT --statisti $ERL_TOP/bin/dialyzer -n -Wunknown -Wunmatched_returns --apps $UNMATCHED --statistics $ERL_TOP/bin/dialyzer -n -Wunknown --apps $NO_UNMATCHED --statistics if [ "X$WARNINGS" != "X" ]; then - $ERL_TOP/bin/dialyzer -n --apps $WARNINGS --statistics + $ERL_TOP/bin/dialyzer -n --apps $WARNINGS --statistics || true fi |