1 files changed, 0 insertions, 16 deletions
diff --git a/src/ci/exec-with-shell.py b/src/ci/exec-with-shell.py
deleted file mode 100755
index 26ce69e33d9..00000000000
--- a/src/ci/exec-with-shell.py
+++ /dev/null
@@ -1,16 +0,0 @@
-#!/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)