diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-04-28 00:20:26 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-04-28 00:20:26 -0400 |
| commit | 3fc61e7f2b84765dc547634463198b30516ed432 (patch) | |
| tree | 2253a14987deca441f3e1bf35a23eb3e3860b9a2 /test | |
| parent | 24093bf30356975b5017613d94bf2927521b666f (diff) | |
travis, please!
Diffstat (limited to 'test')
| -rwxr-xr-x | test/regress/run_regression | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/test/regress/run_regression b/test/regress/run_regression index bf4dcc6ef..f0ffd765d 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -185,6 +185,7 @@ gettemp expoutfile cvc4_expect_stdout.$$.XXXXXXXXXX gettemp experrfile cvc4_expect_stderr.$$.XXXXXXXXXX gettemp outfile cvc4_stdout.$$.XXXXXXXXXX gettemp errfile cvc4_stderr.$$.XXXXXXXXXX +gettemp errfilefix cvc4_stderr.$$.XXXXXXXXXX gettemp exitstatusfile cvc4_exitstatus.$$.XXXXXXXXXX if [ -z "$expected_output" ]; then @@ -247,9 +248,20 @@ else ) > "$outfile" 2> "$errfile" ) fi +# we have to actual error file same treatment as other files. differences in +# versions of echo/bash were causing failure on some platforms and not on others +actual_error=$(cat $errfile) +if [ -z "$actual_error" ]; then + # in case expected stderr output is empty, make sure we don't differ + # by a newline, which we would if we echo "" >"$experrfile" + touch "$errfilefix" +else + echo "$actual_error" >"$errfilefix" +fi + diffs=`diff -u --strip-trailing-cr "$expoutfile" "$outfile"` diffexit=$? -diffserr=`diff -u --strip-trailing-cr "$experrfile" "$errfile"` +diffserr=`diff -u --strip-trailing-cr "$experrfile" "$errfilefix"` diffexiterr=$? exit_status=`cat "$exitstatusfile"` |