]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 67d2755) | patch
do not put " around node name, otherwise names like foo:f1 are not
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 28 Oct 2009 12:19:04 +0000 (12:19 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 28 Oct 2009 12:19:04 +0000 (12:19 +0000)
commit7daf77fac7dc562c3b0a363c7bf4f84d39de4280
tree0d5be8409145d01e27336b9e0f504a2cf63ee852tree | snapshot
parent67d2755f16aea31a10088af9690f664ddfc58c61commit | diff
do not put " around node name, otherwise names like foo:f1 are not
accepted
helm/software/components/extlib/graphvizPp.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.