diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-01-13 17:27:10 +0000 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-01-20 14:46:52 +0000 |
commit | 025c906dd27d00f1cf4e930d138283d711483034 (patch) | |
tree | 59c478a84cf65f36cb966572e61f88e3d3287fd6 /test | |
parent | 0c7f514aebe443db7d46767b1456b421ef591b30 (diff) | |
download | klee-025c906dd27d00f1cf4e930d138283d711483034.tar.gz |
Add lit.local.cfg file for test/Concrete so no tests are executed
in this directory. I don't know why these tests are here, they weren't executed before by DejaGNU.
Diffstat (limited to 'test')
-rw-r--r-- | test/Concrete/lit.local.cfg | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/test/Concrete/lit.local.cfg b/test/Concrete/lit.local.cfg new file mode 100644 index 00000000..b882827d --- /dev/null +++ b/test/Concrete/lit.local.cfg @@ -0,0 +1,3 @@ +# FIXME: Why are these here +# Disable all tests in this directory +config.suffixes = [ ] |