From c734c1b30fd1c58a0d42020859be31d89b92bcd0 Mon Sep 17 00:00:00 2001
From: Sébastien Dailly <sebastien@chimrod.com>
Date: Sat, 9 Jan 2021 11:35:02 +0100
Subject: Moved tools library inside the shapes one

---
 tools/dune | 6 ------
 1 file changed, 6 deletions(-)
 delete mode 100755 tools/dune

(limited to 'tools/dune')

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
-   )
-  )
-- 
cgit v1.2.3