Skip to content

Commit

Permalink
bug-minimizer: link to run-coq-bug-minimizer/actions (#310)
Browse files Browse the repository at this point in the history
This is a small quality of life improvement IMO. Ideally, we'd link
directly to the running job, but that information is not accessible
here, currently.
Zimmi48 authored Sep 13, 2024

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
2 parents 3400bbd + b41f697 commit 0502b0b
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion src/actions.ml
Original file line number Diff line number Diff line change
@@ -2075,10 +2075,11 @@ let run_coq_minimizer ~bot_info ~script ~comment_thread_id ~comment_author
~owner ~repo ~coq_version ~ocaml_version ~minimizer_extra_arguments
>>= function
| Ok () ->
(* TODO: change https://github.com/coq-community/run-coq-bug-minimizer/actions to a link to the particular action run when we can get that information *)
GitHub_mutations.post_comment ~id:comment_thread_id
~message:
(f
"Hey @%s, the coq bug minimizer is running your script, I'll come \
"Hey @%s, the coq bug minimizer [is running](https://github.com/coq-community/run-coq-bug-minimizer/actions) your script, I'll come \
back to you with the results once it's done."
comment_author )
~bot_info

0 comments on commit 0502b0b

Please sign in to comment.