diff options
Diffstat (limited to 'tools/gen-random-bout/Makefile')
| -rw-r--r-- | tools/gen-random-bout/Makefile | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/tools/gen-random-bout/Makefile b/tools/gen-random-bout/Makefile deleted file mode 100644 index 5e1d8cf3..00000000 --- a/tools/gen-random-bout/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -##===- tools/klee/Makefile ---------------*- Makefile -*-===## - -LEVEL=../.. -TOOLNAME = gen-random-bout -USEDLIBS = kleeBasic.a -NO_INSTALL=1 - -include $(LEVEL)/Makefile.common |