diff --git a/tools/with_venv.sh b/tools/with_venv.sh deleted file mode 100755 index 94e05c127d..0000000000 --- a/tools/with_venv.sh +++ /dev/null @@ -1,7 +0,0 @@ -#!/bin/bash -tools_path=${tools_path:-$(dirname $0)} -venv_path=${venv_path:-${tools_path}} -venv_dir=${venv_name:-/../.venv} -TOOLS=${tools_path} -VENV=${venv:-${venv_path}/${venv_dir}} -source ${VENV}/bin/activate && "$@"