From c1676c4bdef09e5c63db79a4988b4fc9008ac374 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Mon, 27 Apr 2020 10:19:53 +0200
Subject: [PATCH] Chore: renaming dirs
---
tools/{ggDeco => gg-deco}/dune | 0
tools/{ggDeco => gg-deco}/ggDeco.ml | 0
tools/{ggDeco => gg-deco}/ggDeco.mli | 0
tools/{ggDeco => gg-deco}/ggDeco_Arg.ml | 0
tools/{ggDeco => gg-deco}/ggDeco_Arg.mli | 0
tools/{ => gg-test}/scriptEnv.py | 0
tools/{ => gg-test}/scriptSkeleton.py | 0
tools/{ => gg-test}/scriptSkeletonProject.py | 0
tools/{test => gg-test}/skeleton/p.ml | 0
tools/{test => gg-test}/skeleton/script0.py | 0
tools/{test => gg-test}/skeleton/script1.py | 0
tools/{test => gg-test}/skeleton/script2_1.py | 0
tools/{test => gg-test}/skeleton/script2_2.py | 0
tools/{test => gg-test}/skeleton/tree.dot | 0
tools/{graphgen => gg}/classicGraph.ml | 0
tools/{graphgen => gg}/classicGraph.mli | 0
tools/{graphgen => gg}/dune | 0
tools/{graphgen => gg}/ggcore.ml | 0
tools/{graphgen => gg}/ggcore.mli | 0
tools/{graphgen => gg}/graphGen.ml | 0
tools/{graphgen => gg}/graphGen_arg.ml | 0
tools/{graphgen => gg}/graphGen_arg.mli | 0
tools/{graphgen => gg}/randomGraph.ml | 0
tools/{graphgen => gg}/randomGraph.mli | 0
tools/{graphgen => gg}/udgUtils.ml | 0
tools/{graphgen => gg}/udgUtils.mli | 0
tools/readme.org | 11 +++++++----
27 files changed, 7 insertions(+), 4 deletions(-)
rename tools/{ggDeco => gg-deco}/dune (100%)
rename tools/{ggDeco => gg-deco}/ggDeco.ml (100%)
rename tools/{ggDeco => gg-deco}/ggDeco.mli (100%)
rename tools/{ggDeco => gg-deco}/ggDeco_Arg.ml (100%)
rename tools/{ggDeco => gg-deco}/ggDeco_Arg.mli (100%)
rename tools/{ => gg-test}/scriptEnv.py (100%)
rename tools/{ => gg-test}/scriptSkeleton.py (100%)
rename tools/{ => gg-test}/scriptSkeletonProject.py (100%)
rename tools/{test => gg-test}/skeleton/p.ml (100%)
rename tools/{test => gg-test}/skeleton/script0.py (100%)
rename tools/{test => gg-test}/skeleton/script1.py (100%)
rename tools/{test => gg-test}/skeleton/script2_1.py (100%)
rename tools/{test => gg-test}/skeleton/script2_2.py (100%)
rename tools/{test => gg-test}/skeleton/tree.dot (100%)
rename tools/{graphgen => gg}/classicGraph.ml (100%)
rename tools/{graphgen => gg}/classicGraph.mli (100%)
rename tools/{graphgen => gg}/dune (100%)
rename tools/{graphgen => gg}/ggcore.ml (100%)
rename tools/{graphgen => gg}/ggcore.mli (100%)
rename tools/{graphgen => gg}/graphGen.ml (100%)
rename tools/{graphgen => gg}/graphGen_arg.ml (100%)
rename tools/{graphgen => gg}/graphGen_arg.mli (100%)
rename tools/{graphgen => gg}/randomGraph.ml (100%)
rename tools/{graphgen => gg}/randomGraph.mli (100%)
rename tools/{graphgen => gg}/udgUtils.ml (100%)
rename tools/{graphgen => gg}/udgUtils.mli (100%)
diff --git a/tools/ggDeco/dune b/tools/gg-deco/dune
similarity index 100%
rename from tools/ggDeco/dune
rename to tools/gg-deco/dune
diff --git a/tools/ggDeco/ggDeco.ml b/tools/gg-deco/ggDeco.ml
similarity index 100%
rename from tools/ggDeco/ggDeco.ml
rename to tools/gg-deco/ggDeco.ml
diff --git a/tools/ggDeco/ggDeco.mli b/tools/gg-deco/ggDeco.mli
similarity index 100%
rename from tools/ggDeco/ggDeco.mli
rename to tools/gg-deco/ggDeco.mli
diff --git a/tools/ggDeco/ggDeco_Arg.ml b/tools/gg-deco/ggDeco_Arg.ml
similarity index 100%
rename from tools/ggDeco/ggDeco_Arg.ml
rename to tools/gg-deco/ggDeco_Arg.ml
diff --git a/tools/ggDeco/ggDeco_Arg.mli b/tools/gg-deco/ggDeco_Arg.mli
similarity index 100%
rename from tools/ggDeco/ggDeco_Arg.mli
rename to tools/gg-deco/ggDeco_Arg.mli
diff --git a/tools/scriptEnv.py b/tools/gg-test/scriptEnv.py
similarity index 100%
rename from tools/scriptEnv.py
rename to tools/gg-test/scriptEnv.py
diff --git a/tools/scriptSkeleton.py b/tools/gg-test/scriptSkeleton.py
similarity index 100%
rename from tools/scriptSkeleton.py
rename to tools/gg-test/scriptSkeleton.py
diff --git a/tools/scriptSkeletonProject.py b/tools/gg-test/scriptSkeletonProject.py
similarity index 100%
rename from tools/scriptSkeletonProject.py
rename to tools/gg-test/scriptSkeletonProject.py
diff --git a/tools/test/skeleton/p.ml b/tools/gg-test/skeleton/p.ml
similarity index 100%
rename from tools/test/skeleton/p.ml
rename to tools/gg-test/skeleton/p.ml
diff --git a/tools/test/skeleton/script0.py b/tools/gg-test/skeleton/script0.py
similarity index 100%
rename from tools/test/skeleton/script0.py
rename to tools/gg-test/skeleton/script0.py
diff --git a/tools/test/skeleton/script1.py b/tools/gg-test/skeleton/script1.py
similarity index 100%
rename from tools/test/skeleton/script1.py
rename to tools/gg-test/skeleton/script1.py
diff --git a/tools/test/skeleton/script2_1.py b/tools/gg-test/skeleton/script2_1.py
similarity index 100%
rename from tools/test/skeleton/script2_1.py
rename to tools/gg-test/skeleton/script2_1.py
diff --git a/tools/test/skeleton/script2_2.py b/tools/gg-test/skeleton/script2_2.py
similarity index 100%
rename from tools/test/skeleton/script2_2.py
rename to tools/gg-test/skeleton/script2_2.py
diff --git a/tools/test/skeleton/tree.dot b/tools/gg-test/skeleton/tree.dot
similarity index 100%
rename from tools/test/skeleton/tree.dot
rename to tools/gg-test/skeleton/tree.dot
diff --git a/tools/graphgen/classicGraph.ml b/tools/gg/classicGraph.ml
similarity index 100%
rename from tools/graphgen/classicGraph.ml
rename to tools/gg/classicGraph.ml
diff --git a/tools/graphgen/classicGraph.mli b/tools/gg/classicGraph.mli
similarity index 100%
rename from tools/graphgen/classicGraph.mli
rename to tools/gg/classicGraph.mli
diff --git a/tools/graphgen/dune b/tools/gg/dune
similarity index 100%
rename from tools/graphgen/dune
rename to tools/gg/dune
diff --git a/tools/graphgen/ggcore.ml b/tools/gg/ggcore.ml
similarity index 100%
rename from tools/graphgen/ggcore.ml
rename to tools/gg/ggcore.ml
diff --git a/tools/graphgen/ggcore.mli b/tools/gg/ggcore.mli
similarity index 100%
rename from tools/graphgen/ggcore.mli
rename to tools/gg/ggcore.mli
diff --git a/tools/graphgen/graphGen.ml b/tools/gg/graphGen.ml
similarity index 100%
rename from tools/graphgen/graphGen.ml
rename to tools/gg/graphGen.ml
diff --git a/tools/graphgen/graphGen_arg.ml b/tools/gg/graphGen_arg.ml
similarity index 100%
rename from tools/graphgen/graphGen_arg.ml
rename to tools/gg/graphGen_arg.ml
diff --git a/tools/graphgen/graphGen_arg.mli b/tools/gg/graphGen_arg.mli
similarity index 100%
rename from tools/graphgen/graphGen_arg.mli
rename to tools/gg/graphGen_arg.mli
diff --git a/tools/graphgen/randomGraph.ml b/tools/gg/randomGraph.ml
similarity index 100%
rename from tools/graphgen/randomGraph.ml
rename to tools/gg/randomGraph.ml
diff --git a/tools/graphgen/randomGraph.mli b/tools/gg/randomGraph.mli
similarity index 100%
rename from tools/graphgen/randomGraph.mli
rename to tools/gg/randomGraph.mli
diff --git a/tools/graphgen/udgUtils.ml b/tools/gg/udgUtils.ml
similarity index 100%
rename from tools/graphgen/udgUtils.ml
rename to tools/gg/udgUtils.ml
diff --git a/tools/graphgen/udgUtils.mli b/tools/gg/udgUtils.mli
similarity index 100%
rename from tools/graphgen/udgUtils.mli
rename to tools/gg/udgUtils.mli
diff --git a/tools/readme.org b/tools/readme.org
index 2b618272..4ce40b46 100644
--- a/tools/readme.org
+++ b/tools/readme.org
@@ -1,6 +1,9 @@
-Some experimental but yet useful tools by Nathan Rébiscoul and Gwennan
-Eliezer (undergraduate trainees).
+Various tools to use with =sasa=
-- =gg= is a dot graph generator.
-- =gg-deco= decorates graphs generated by =gg=
+- =rdbgui= is a GUI dedicated to the use of =sasa= with =rdbg=
+- =gg= is a dot graph generator (*).
+- =gg-deco= decorates graphs generated by =gg= (*)
+
+(*) experimental but yet useful tools implemented by Nathan Rébiscoul
+and Gwennan Eliezer (undergraduate trainees).
--
GitLab