diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-09-28 19:59:47 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-28 19:59:47 -0700 |
| commit | 1c1add20d0842ea347fffb19bb3ad90eee665a3b (patch) | |
| tree | b1226ff683227bf0a37b262c34e5eca64ba0babe | |
| parent | d84c92f254c722c0307267a866a5a3e8430bcd35 (diff) | |
contrib: Fix check for get-script-header.sh. (#7259)
PR #7219 removed CVC language support and therefore also the file src/parser/cvc/Cvc.g. This commit fixes the check (and the nightlies).
| -rw-r--r-- | contrib/get-script-header.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/get-script-header.sh b/contrib/get-script-header.sh index 5deaa00da..49af8d887 100644 --- a/contrib/get-script-header.sh +++ b/contrib/get-script-header.sh @@ -12,7 +12,7 @@ INSTALL_BIN_DIR="$INSTALL_DIR/bin" mkdir -p "$DEPS_DIR" -if ! [ -e src/parser/cvc/Cvc.g ]; then +if ! [ -e src/parser/smt2/Smt2.g ]; then echo "$(basename $0): I expect to be in the contrib/ of a cvc5 source tree," >&2 echo "but apparently:" >&2 echo >&2 |