From 9beb8f54774ca0d41dd2eb7622809f4073676757 Mon Sep 17 00:00:00 2001 From: Pietro Albini Date: Tue, 26 Nov 2019 12:06:30 +0100 Subject: ci: add github actions configuration --- src/ci/exec-with-shell.py | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100755 src/ci/exec-with-shell.py (limited to 'src/ci/exec-with-shell.py') diff --git a/src/ci/exec-with-shell.py b/src/ci/exec-with-shell.py new file mode 100755 index 00000000000..26ce69e33d9 --- /dev/null +++ b/src/ci/exec-with-shell.py @@ -0,0 +1,16 @@ +#!/usr/bin/env python +# A simple wrapper that forwards the arguments to bash, unless the +# CI_OVERRIDE_SHELL environment variable is present: in that case the content +# of that environment variable is used as the shell path. + +import os +import sys +import subprocess + +try: + shell = os.environ["CI_OVERRIDE_SHELL"] +except KeyError: + shell = "bash" + +res = subprocess.call([shell] + sys.argv[1:]) +sys.exit(res) -- cgit 1.4.1-3-g733a5