aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rwxr-xr-xscripts/run-dialyzer2
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