New: add graph attributes in the decorated graph
Showing
- tools/ggDeco/ggDeco.ml 40 additions, 18 deletionstools/ggDeco/ggDeco.ml
- tools/ggDeco/ggDeco_Arg.ml 76 additions, 55 deletionstools/ggDeco/ggDeco_Arg.ml
- tools/graphgen/classicGraph.ml 8 additions, 3 deletionstools/graphgen/classicGraph.ml
- tools/graphgen/graphGen.ml 95 additions, 19 deletionstools/graphgen/graphGen.ml
- tools/graphgen/graphGen_arg.ml 57 additions, 45 deletionstools/graphgen/graphGen_arg.ml
Loading
Please register or sign in to comment