diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-09-26 22:22:09 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-09-26 22:22:09 +0000 |
| commit | 868ee6deae0febd3dbdc319d114536d50f7e3b41 (patch) | |
| tree | fb421832dd7901fed33ec4dc4a6ab612f6e66361 /src/options | |
| parent | b06a3d697c1dc57c58498c9e8612d4c21d6395d6 (diff) | |
disable building of cvc3_george system-test object (which isn't used yet anyway, and required ~10 minutes to build with -O3).
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/options')
0 files changed, 0 insertions, 0 deletions