diff options
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 |
