diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-03-09 10:33:32 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-09 12:33:32 -0500 |
| commit | c1da31ed532cd1767c20d5fc01df893c427e0e8e (patch) | |
| tree | 6904b8d264f7d5f8be7288be836c3455c6ef51f9 /src/theory/strings/word.cpp | |
| parent | 31e30d52a3fc6ac2a2a2f5e8d4a17a4ca954d8e8 (diff) | |
Fix quoting of options on Travis (#3981)
For some reason, Travis has started to treat our `TRAVIS_CVC4_CONFIG`
environment variable wrong, leading to failing builds. Travis started to
wrap the argument into double quotes, so when we had single quotes
around our argument list, the arguments were treated as a single
argument and when we had double quotes, the second pair of double quotes
terminated the first one permaturely. Declaring the environment
variables individually seems to work as expected, so this commit is
moving to that format.
Diffstat (limited to 'src/theory/strings/word.cpp')
0 files changed, 0 insertions, 0 deletions