From d080c822cf26b5a8d922966fa123466bc49831ba Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky>
Date: Thu, 6 Oct 2005 06:08:11 +0000
Subject: [PATCH] fix generation of graph files

---
 Repair/RepairCompiler/MCC/IR/GraphNode.java | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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()) {
-- 
2.34.1