diff --git a/run-mypy.sh b/run-mypy.sh new file mode 100755 index 0000000000000000000000000000000000000000..43e64854d17710b3e5835c6fe8f2624b9708f162 --- /dev/null +++ b/run-mypy.sh @@ -0,0 +1,3 @@ +#! /bin/bash + +mypy pytools