fix generation of graph files

diff --git a/Repair/RepairCompiler/MCC/IR/GraphNode.java b/Repair/RepairCompiler/MCC/IR/GraphNode.java
index a450745bd132d11f9b3183b84f5fa2b841c8e791..80d34a9a5ac626a786e6c2fcc5a2212b1ed73834 100755 (executable)
--- 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()) {