diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-09-04 14:59:19 -0700 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-04 16:59:19 -0500 |
| commit | 747a9a248da073911e1c0da34c38f0648421a087 (patch) | |
| tree | 98449a71c66d0ad427b8c8dc6f0ed1b9fbccdfbe /src/compat/Makefile | |
| parent | 29bf7d6a937ab50c4dd92a30d7beb36a4001ead6 (diff) | |
Remove CVC3 compatibility layer (#2418)
Diffstat (limited to 'src/compat/Makefile')
| -rw-r--r-- | src/compat/Makefile | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/src/compat/Makefile b/src/compat/Makefile deleted file mode 100644 index 675bd8827..000000000 --- a/src/compat/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../.. -srcdir = src/compat - -include $(topdir)/Makefile.subdir |