diff options
Diffstat (limited to 'tools/check_source.sh')
-rwxr-xr-x | tools/check_source.sh | 15 |
1 files changed, 0 insertions, 15 deletions
diff --git a/tools/check_source.sh b/tools/check_source.sh deleted file mode 100755 index de8c790..0000000 --- a/tools/check_source.sh +++ /dev/null @@ -1,15 +0,0 @@ -#!/bin/sh - - -set -euf - - -script="$(realpath "$0")" -tools="$(dirname "$script")" -root="$(dirname "$tools")" - - -black "$root" -mypy --strict "$root" -flake8 "$root" -pytest "$root" |