summaryrefslogtreecommitdiffstats
path: root/bin/dune
diff options
context:
space:
mode:
authorScott Lawrence <scott+git@ineffectivetheory.com>2024-06-26 21:16:48 -0700
committerScott Lawrence <scott+git@ineffectivetheory.com>2024-06-26 21:16:48 -0700
commitede8966c44cca6854012078329482a70235a19ce (patch)
tree3e6629114cc11037a6364b30e6c63c402d3ccca6 /bin/dune
parenta4c197dea1a0192b93e205daf8738f99a4f039b2 (diff)
downloadagate-main.tar.gz
agate-main.tar.bz2
agate-main.zip
Deleted everything but the one scriptHEADmain
Diffstat (limited to 'bin/dune')
-rw-r--r--bin/dune4
1 files changed, 0 insertions, 4 deletions
diff --git a/bin/dune b/bin/dune
deleted file mode 100644
index 3891864..0000000
--- a/bin/dune
+++ /dev/null
@@ -1,4 +0,0 @@
-(executable
- (public_name agate)
- (name main)
- (libraries agate angstrom))