From 9bb703e9ad738f9e5380d1e8e69cb4e36bed2366 Mon Sep 17 00:00:00 2001 From: Steven Arcangeli Date: Mon, 28 Aug 2023 18:28:00 -0700 Subject: tools: split fast and slow lint commands --- .github/pre-commit | 2 +- .github/pre-push | 4 ++++ 2 files changed, 5 insertions(+), 1 deletion(-) create mode 100755 .github/pre-push (limited to '.github') diff --git a/.github/pre-commit b/.github/pre-commit index 240abeb..c64fbec 100755 --- a/.github/pre-commit +++ b/.github/pre-commit @@ -1,3 +1,3 @@ #!/bin/bash set -e -make lint +make fastlint diff --git a/.github/pre-push b/.github/pre-push new file mode 100755 index 0000000..b837eec --- /dev/null +++ b/.github/pre-push @@ -0,0 +1,4 @@ +#!/bin/bash +set -e +make lint +make test -- cgit v1.2.3-70-g09d2