sparse-intern-71089
03/29/2022, 3:24 AMbusy-island-31180
03/29/2022, 3:30 AM// It’s not entirely clear how to treat PR deletion according to Terraform’s
// CRUD semantics. The approach we’re taking here is to close the PR unless
// it’s already closed or merged. Merging it feels intuitively wrong in what
// effectively is a destructor.https://github.com/integrations/terraform-provider-github/blob/main/github/resource_github_repository_pull_request.go#L256 I guess this makes sense.