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/Makefile.am | |
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/Makefile.am')
0 files changed, 0 insertions, 0 deletions