From: Claudio Sacerdoti Coen Date: Mon, 19 Jan 2004 14:26:22 +0000 (+0000) Subject: We are now using the standard dot distribution of debian. X-Git-Tag: V_0_5_1_3~23 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dcfdf34d7b60c987b1686cadb338fc490c4d7487;p=helm.git We are now using the standard dot distribution of debian. --- diff --git a/helm/graphs/tools/Makefile b/helm/graphs/tools/Makefile index 48f035454..1d945f8fd 100644 --- a/helm/graphs/tools/Makefile +++ b/helm/graphs/tools/Makefile @@ -1,6 +1,7 @@ PID= -DOT=../gv1.7c/bin/dot -SED=sed "s/font-family:Times;//g" +DOT=dot +#SED=sed "s/font-family:Times;//g" +SED=cat REQUIRES = http PREDICATES = mt