Skip to content

Commit 7db6b5a

Browse files
authored
Post a comment when the bug minimizer fails to start, even when not in CI mode (#319)
2 parents d0300d7 + 0ed5c81 commit 7db6b5a

File tree

1 file changed

+11
-2
lines changed

1 file changed

+11
-2
lines changed

src/actions.ml

+11-2
Original file line numberDiff line numberDiff line change
@@ -2086,8 +2086,17 @@ let run_coq_minimizer ~bot_info ~script ~comment_thread_id ~comment_author
20862086
comment_author )
20872087
~bot_info
20882088
>>= GitHub_mutations.report_on_posting_comment
2089-
| Error f ->
2090-
Lwt_io.printf "Error: %s\n" f
2089+
| Error e ->
2090+
Lwt_io.printf "Error: %s\n" e
2091+
>>= fun () ->
2092+
GitHub_mutations.post_comment ~id:comment_thread_id
2093+
~message:
2094+
(f
2095+
"Error encountered when attempting to start the coq bug minimizer:\n\
2096+
%s\n\n\
2097+
cc @JasonGross" e)
2098+
~bot_info
2099+
>>= GitHub_mutations.report_on_posting_comment
20912100

20922101
let coq_bug_minimizer_results_action ~bot_info ~ci ~key ~app_id body =
20932102
if string_match ~regexp:"\\([^\n]+\\)\n\\([^\r]*\\)" body then

0 commit comments

Comments
 (0)