Fix undefined term in Github workflows

This commit is contained in:
Jean-Michel Picod
2020-02-24 19:31:37 +01:00
parent b18d3097a3
commit a73837cb59

View File

@@ -15,6 +15,9 @@
set -e set -e
# Ensure the script doesn't fail on Github workflows
TERM=${TERM:-vt100}
# Check that rustup and pip3 are installed # Check that rustup and pip3 are installed
check_command () { check_command () {
if ! which "$1" >/dev/null if ! which "$1" >/dev/null