aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorChimrod <>2024-01-14 12:11:45 +0100
committerChimrod <>2024-01-14 12:23:21 +0100
commitc6dbbaa9e11c34330315f614d922da8ede5824aa (patch)
tree84164d9888a09b80f672516e9158555c84997957
parent0f9f5d50bd04e23956e3c84359042659ed25149f (diff)
Also include the debugs messages in the exit code
-rw-r--r--bin/qsp_parser.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/bin/qsp_parser.ml b/bin/qsp_parser.ml
index 1e897a0..5a34ab2 100644
--- a/bin/qsp_parser.ml
+++ b/bin/qsp_parser.ml
@@ -150,9 +150,9 @@ let () =
in
match (!ctx.error_nb, !ctx.warn_nb) with
- | 0, 0 ->
+ | 0, 0 -> (
print_endline "No errors found";
- exit 0
+ match !ctx.debug_nb with 0 -> exit 0 | _ -> exit 1)
| _ ->
Printf.printf "Found %d error(s), %d warning(s)\n" !ctx.error_nb
!ctx.warn_nb;