diff --git a/maintenance/tools-pull.sh b/maintenance/tools-pull.sh deleted file mode 100755 index 26ca3c2..0000000 --- a/maintenance/tools-pull.sh +++ /dev/null @@ -1,4 +0,0 @@ -#!/usr/bin/env bash -set -euo pipefail - -echo "TODO"