diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-06-21 10:55:03 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-06-21 10:55:03 -0700 |
| commit | cf9dfb9be23b4f802989fecd18756ed62aecc8e4 (patch) | |
| tree | 3f1f45759bf85b451b458aab98cf62892f7aef17 /src/util/CMakeLists.txt | |
| parent | 073335156ff7644364d12a91d4d41af776cfb91b (diff) | |
Use TMPDIR environment variable for temp files (#2849)
Previously, we were just writing temporary files to `/tmp/` but this
commit allows the user to use the `TMPDIR` environment variable to
determine which directory the temporary file should be written to. The
commit adds a helper function for this and also includes some minor
cleanup of existing code.
Diffstat (limited to 'src/util/CMakeLists.txt')
| -rw-r--r-- | src/util/CMakeLists.txt | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index a17f7c510..f107ad95f 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -47,6 +47,7 @@ libcvc4_add_sources( statistics_registry.h tuple.h unsafe_interrupt_exception.h + utility.cpp utility.h ) |