From: bdemsky <bdemsky>
Date: Thu, 6 Oct 2005 06:08:11 +0000 (+0000)
Subject: fix generation of graph files
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=d080c822cf26b5a8d922966fa123466bc49831ba;p=repair.git

fix generation of graph files
---

diff --git a/Repair/RepairCompiler/MCC/IR/GraphNode.java b/Repair/RepairCompiler/MCC/IR/GraphNode.java
index a450745..80d34a9 100755
--- a/Repair/RepairCompiler/MCC/IR/GraphNode.java
+++ b/Repair/RepairCompiler/MCC/IR/GraphNode.java
@@ -75,7 +75,7 @@ public class GraphNode {
     String nodeoption="";
 
     public void setOption(String option) {
-	this.nodeoption=option;
+	this.nodeoption=","+option;
     }
 
     public void setMerge() {
@@ -276,7 +276,7 @@ public class GraphNode {
 		if (special!=null&&special.contains(gn))
 		    option+=",shape=box";
 		if (!gn.merge)
-		    output.println("\t" + gn.getLabel() + " [label=\"" + label + "\"" + gn.dotnodeparams + option+"];");
+                    output.println("\t" + gn.getLabel() + " [label=\"" + label + "\"" + gn.dotnodeparams + option+"];");
 
 		if (!gn.merge)
                 while (edges.hasNext()) {