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 2b618272d0bd26e6bae86e3f379422ef323e7d04..4ce40b460f08e39146f5b3067d9b32bf4297552d 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).