Subject: Re: [PATCH] ci: update coverity runs_on_pool reference

From: Patrick Steinhardt <[email-masked]>
Date: Fri, 10 May 2024 06:31:25 +0200

On Thu, May 09, 2024 at 12:15:06PM -0400, Jeff King wrote:
> Commit 2d65e5b6a6 (ci: rename "runs_on_pool" to "distro", 2024-04-12)
> renamed this variable for the main CI workflow, as well as in the ci/
> scripts. Because the coverity workflow also relies on those scripts to
> install dependencies, it needs to be updated, too. Without this patch,
> the coverity build fails because we lack libcurl.

Ah, I missed that one. Thanks for the fix, which looks obviously good to
me!

Patrick