diff --git a/bot-components/GitHub_queries.ml b/bot-components/GitHub_queries.ml index 691d97ea..da9473ec 100644 --- a/bot-components/GitHub_queries.ml +++ b/bot-components/GitHub_queries.ml @@ -267,6 +267,7 @@ let closer_info_option_of_closer closer = | None -> Ok ClosedByCommit | Some prs -> ( match prs#nodes with + | Some [] -> Ok ClosedByCommit | Some [Some pr] -> Ok (ClosedByPullRequest (closer_info_of_pr pr)) | Some (_ :: _) -> Error "Closing commit associated to several pull requests."