Fix: use simpler GraphQL query when only ID is needed.

Will help reduce the impact of #303.
coq · Jun 17, 2024 · b95de99 · b95de99
1 parent 7f42acb
commit b95de99
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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