aboutsummaryrefslogtreecommitdiffstats
path: root/debug/dune
diff options
context:
space:
mode:
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))