From b95de99a33d1f61259e09d66fba5bcf17deb007f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Mon, 17 Jun 2024 11:09:46 +0200 Subject: [PATCH] =?UTF-8?q?Fix:=20use=20simpler=20GraphQL=20query=20when?= =?UTF-8?q?=20only=20ID=C2=A0is=20needed.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Will help reduce the impact of #303. --- bot-components/GitHub_queries.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/bot-components/GitHub_queries.ml b/bot-components/GitHub_queries.ml index 96f99d31..7e897591 100644 --- a/bot-components/GitHub_queries.ml +++ b/bot-components/GitHub_queries.ml @@ -180,7 +180,7 @@ let get_pull_request_id_and_milestone ~bot_info ~owner ~repo ~number = None ) ) ) ) let get_pull_request_id ~bot_info ~owner ~repo ~number = - let open GitHub_GraphQL.PullRequest_ID_and_Milestone in + let open GitHub_GraphQL.PullRequest_ID in makeVariables ~owner ~repo ~number () |> serializeVariables |> variablesToJson |> send_graphql_query ~bot_info ~query