summaryrefslogtreecommitdiff
path: root/tools/dune
diff options
context:
space:
mode:
Diffstat (limited to 'tools/dune')
-rwxr-xr-xtools/dune6
1 files changed, 0 insertions, 6 deletions
diff --git a/tools/dune b/tools/dune
deleted file mode 100755
index a2c3fdb..0000000
--- a/tools/dune
+++ /dev/null
@@ -1,6 +0,0 @@
-(library
- (name tools)
- (libraries
- gg
- )
- )