aboutsummaryrefslogtreecommitdiffstats
path: root/debug/dune
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-12-09 20:03:41 +0000
committerYann Herklotz <git@yannherklotz.com>2021-12-09 20:03:41 +0000
commita64ccb64e16175b520a0dc4badde44a1cc46f17d (patch)
tree41ff3b4511e40a809f1fefb4e0c02da643de92ad /debug/dune
parent1c91db6b6d4cd20994fdfc40283b003c1ec93d50 (diff)
downloadvericert-a64ccb64e16175b520a0dc4badde44a1cc46f17d.tar.gz
vericert-a64ccb64e16175b520a0dc4badde44a1cc46f17d.zip
Remove debug directory
Diffstat (limited to 'debug/dune')
-rw-r--r--debug/dune5
1 files changed, 0 insertions, 5 deletions
diff --git a/debug/dune b/debug/dune
deleted file mode 100644
index feee97c..0000000
--- a/debug/dune
+++ /dev/null
@@ -1,5 +0,0 @@
-(include_subdirs no)
-
-(executable
- (name VericertTest)
- (libraries vericert))