Files
ISSOtm fa22b78e7d Use type instead of which in shell scripts
The latter is not a Bash built-in,
and some environments turn out to produce non-conforming
return codes.

`type` is provided by Bash itself,
so we can rely on it better.
2026-05-05 16:03:33 +02:00
..
2026-04-16 00:57:33 +02:00
2026-04-16 00:25:58 +02:00