diff options
author | Sébastien Dailly <sebastien@chimrod.com> | 2021-01-09 11:35:02 +0100 |
---|---|---|
committer | Sébastien Dailly <sebastien@chimrod.com> | 2021-01-09 11:35:02 +0100 |
commit | c734c1b30fd1c58a0d42020859be31d89b92bcd0 (patch) | |
tree | c5a8e7e04347122f759d651f63e042b73e4b9f5b | |
parent | 32618a5ce8e2b306af102e4c16711b090c36b840 (diff) |
Moved tools library inside the shapes one
-rwxr-xr-x | shapes/tools/dune (renamed from tools/dune) | 0 | ||||
-rwxr-xr-x | shapes/tools/utils.ml (renamed from tools/utils.ml) | 0 | ||||
-rwxr-xr-x | shapes/tools/utils.mli (renamed from tools/utils.mli) | 0 |
3 files changed, 0 insertions, 0 deletions
diff --git a/tools/dune b/shapes/tools/dune index a2c3fdb..a2c3fdb 100755 --- a/tools/dune +++ b/shapes/tools/dune diff --git a/tools/utils.ml b/shapes/tools/utils.ml index b8a473f..b8a473f 100755 --- a/tools/utils.ml +++ b/shapes/tools/utils.ml diff --git a/tools/utils.mli b/shapes/tools/utils.mli index 4e12906..4e12906 100755 --- a/tools/utils.mli +++ b/shapes/tools/utils.mli |