aboutsummaryrefslogtreecommitdiff
path: root/.run_formal_checks.sh
diff options
context:
space:
mode:
authorJack Koenig2021-08-02 14:28:19 -0700
committerGitHub2021-08-02 14:28:19 -0700
commitc0479d9ace45e7e91bb7de96deb8ab6df98799f7 (patch)
treead4771a6a0bac93aa389e02fad6881f3464b38e2 /.run_formal_checks.sh
parent782a84a0161f95c137229870e0b20eb0520c36e9 (diff)
Skip Formal CI checks via Github Actions not commit message (#2308)
Diffstat (limited to '.run_formal_checks.sh')
-rwxr-xr-x.run_formal_checks.sh10
1 files changed, 2 insertions, 8 deletions
diff --git a/.run_formal_checks.sh b/.run_formal_checks.sh
index 0a28a1d1..3451c688 100755
--- a/.run_formal_checks.sh
+++ b/.run_formal_checks.sh
@@ -21,14 +21,8 @@ if [ ! -z "$GITHUB_BASE_REF" ]; then
git remote set-branches origin $GITHUB_BASE_REF && git fetch
git checkout $GITHUB_BASE_REF
git checkout -
- # Skip if '[skip formal checks]' shows up in any of the commit messages in the PR
- if git log --format=%B --no-merges $GITHUB_BASE_REF..HEAD | grep '\[skip formal checks\]'; then
- echo "Commit message says to skip formal checks"
- exit 0
- else
- cp regress/$DUT.fir $DUT.fir
- ./scripts/formal_equiv.sh HEAD $GITHUB_BASE_REF $DUT
- fi
+ cp regress/$DUT.fir $DUT.fir
+ ./scripts/formal_equiv.sh HEAD $GITHUB_BASE_REF $DUT
else
echo "Not a pull request, no formal check"
exit 0