Pietro Albini fde5811d74 ci: use bash when executing the "bors build finished" jobs ... We don't clone the repository in those builders, so the default shell (src/ci/exec-with-shell.py) is not present there.		2020-04-29 16:32:32 +02:00
..
ISSUE_TEMPLATE
workflows	ci: use bash when executing the "bors build finished" jobs	2020-04-29 16:32:32 +02:00