diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-07-15 13:15:24 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-15 06:15:24 -0500 |
| commit | a482635216017b0d558229f2339c663cf58f8d23 (patch) | |
| tree | 12dd4ef743ccb6e5c19afee1e482833dbdced0c2 /src | |
| parent | eb58f1ef8917c5d57d64c54f9188b0ed489b47c1 (diff) | |
Add missing header (Fixes #4743) (#4749)
Thanks to Dejan for this hint (in #4743)
Diffstat (limited to 'src')
| -rw-r--r-- | src/CMakeLists.txt | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index af2d0b782..199c14330 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -959,6 +959,7 @@ install(FILES expr/emptyset.h expr/expr_iomanip.h expr/record.h + expr/sequence.h expr/symbol_table.h expr/type.h expr/uninterpreted_constant.h |