aboutsummaryrefslogtreecommitdiffstats
path: root/debug/dune
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-05-03 17:13:56 +0100
committerYann Herklotz <git@yannherklotz.com>2020-05-03 17:13:56 +0100
commit0b118f8dca9068e0075e72f4d0c24cf707df44c7 (patch)
tree4697b2ce306c4271b92a46589685603d62a0848a /debug/dune
parentd2c3d5a4fdb35b861be9df0795ef83f9b83c7bb7 (diff)
downloadvericert-kvx-0b118f8dca9068e0075e72f4d0c24cf707df44c7.tar.gz
vericert-kvx-0b118f8dca9068e0075e72f4d0c24cf707df44c7.zip
Add code to debug execution of HLSsave/old-step
Diffstat (limited to 'debug/dune')
-rw-r--r--debug/dune5
1 files changed, 5 insertions, 0 deletions
diff --git a/debug/dune b/debug/dune
new file mode 100644
index 0000000..7f0c6a6
--- /dev/null
+++ b/debug/dune
@@ -0,0 +1,5 @@
+(include_subdirs no)
+
+(executable
+ (name CoqupTest)
+ (libraries coqup))