diff options
| author | Jack Koenig | 2021-08-02 14:28:19 -0700 |
|---|---|---|
| committer | GitHub | 2021-08-02 14:28:19 -0700 |
| commit | c0479d9ace45e7e91bb7de96deb8ab6df98799f7 (patch) | |
| tree | ad4771a6a0bac93aa389e02fad6881f3464b38e2 /.run_formal_checks.sh | |
| parent | 782a84a0161f95c137229870e0b20eb0520c36e9 (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.sh | 10 |
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 |
