]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9ed9bdd) | patch
- enable header to output graphs attributes and graph-wide node and edge
authorStefano Zacchiroli <zack@upsilon.cc>
Wed, 19 Jul 2006 17:29:44 +0000 (17:29 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Wed, 19 Jul 2006 17:29:44 +0000 (17:29 +0000)
commit0ece452577dc3d9e593c862c0531367aa6d8840a
treeadfe3192a009c5a702812a0854eb783ed1fed577tree | snapshot
parent9ed9bdd5f158f092114c2d98c2537a9396d6a8d7commit | diff
- enable header to output graphs attributes and graph-wide node and edge
  attributes
- quote nodes only when needed
components/extlib/graphvizPp.ml diff | blob | history
components/extlib/graphvizPp.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.