]> matita.cs.unibo.it Git - helm.git/commitdiff
We are now using the standard dot distribution of debian.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 19 Jan 2004 14:26:22 +0000 (14:26 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 19 Jan 2004 14:26:22 +0000 (14:26 +0000)
helm/graphs/tools/Makefile

index 48f035454070f87eaf0248c52bc6a694a8fc0a54..1d945f8fd66e8abb350a93cf26df7be76b0606fd 100644 (file)
@@ -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