Re: [PATCH] ci: skip unavailable external software

[Junio C Hamano <gitster@pobox.com>]

Johannes Schindelin <Johannes.Schindelin@gmx.de> writes:

> That is true. It would probably also make sense to mark the message as a
> `::warning::` on GitHub (and the equivalent on GitLab), so that it is
> shown a bit more prominently in the CI summary.

::warning:: may be a good idea, but I actually think we should
remove the message when we say "ah wget && chmod failed, so let's
remove".  At the end of the same script, there already is "ah jgit
is not there, so let's warn" code exists (and it would falsely say
"jgit file exists but cannot be executed" and take the whole thing
down if we do not remove after a failed download).  The ::warning::
should belong there.

Thanks.