diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-06-18 23:09:29 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-06-18 23:09:29 +0000 |
commit | 498bb02fc7d2539d41b778bc42e383ca8dbf6d9e (patch) | |
tree | a4192c19dd6f28a2547b647ffb1a385ac3e7b802 /src/theory | |
parent | fd6af9181e763cd9564245114cfa47f3952484db (diff) |
"statistics" and "staticbinary" are now tags on the build (so you get build directories like builds/x86_64-unknown-linux-gnu/debug-staticbinary-nostatistics .. etc. This is useful to distinguish static binary builds and statistics builds from each other when you configure multiple times in the same source directory
Diffstat (limited to 'src/theory')
0 files changed, 0 insertions, 0 deletions