diff --git a/test/watchdog.ml b/test/watchdog.ml index 99c9040..dbc10b8 100644 --- a/test/watchdog.ml +++ b/test/watchdog.ml @@ -39,6 +39,8 @@ let dying _ = \ turned into a failing run.\n" !label !budget; flush stderr; + (* [exit] rather than [_exit]: the rows that did pass are in stdout's buffer + and a watchdog that threw them away would be worse than the hang. *) exit 2 (* Re-arm the backstop for whatever is left of its budget. One second is the