diff options
| author | Patrick Steinhardt <ps@pks.im> | 2024-04-12 06:43:57 +0200 |
|---|---|---|
| committer | Junio C Hamano <gitster@pobox.com> | 2024-04-12 08:47:49 -0700 |
| commit | 2d65e5b6a624e9642c4d765a861cf291095adc72 (patch) | |
| tree | 94a68a1572c2925fc0461e943e60534a2187c29f /commit.c | |
| parent | 19981daefd7c147444462739375462b49412ce33 (diff) | |
ci: rename "runs_on_pool" to "distro"
The "runs_on_pool" environment variable is used by our CI scripts to
distinguish the different kinds of operating systems. It is quite
specific to GitHub Actions though and not really a descriptive name.
Rename the variable to "distro" to clarify its intent.
Signed-off-by: Patrick Steinhardt <ps@pks.im>
Signed-off-by: Junio C Hamano <gitster@pobox.com>
Diffstat (limited to 'commit.c')
0 files changed, 0 insertions, 0 deletions