From 458c4490ce68f5b3d94e7bba6f1cfd9c82ee2fda Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?=
 <theo.zimmermann@univ-paris-diderot.fr>
Date: Fri, 1 Nov 2019 10:53:12 +0100
Subject: [PATCH] Empty list in query answer is OK.

---
 bot-components/GitHub_queries.ml | 1 +
 1 file changed, 1 insertion(+)

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."