Empty list in query answer is OK.

coq · Nov 1, 2019 · 458c449 · 458c449
1 parent 9e8ac70
commit 458c449
Showing 1 changed file with 1 addition and 0 deletions.
diff --git 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."