MOVEDlint: exit 1 in case of error

2022-08-23 14:48:35 +02:00 · 2022-08-23 14:48:35 +02:00 · abe88637f5
commit abe88637f5
parent 85397ca391
1 changed files with 2 additions and 0 deletions
--- a/Tools/scripts/MOVEDlint.awk
+++ b/Tools/scripts/MOVEDlint.awk
@ -173,4 +173,6 @@ END {
    }

    close(sort)
+    if (length(error) > 0)
+	    exit(1)
 }