From 81b1bd6ac5433b8bb4c2bc20411e86552707dbac Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky>
Date: Wed, 18 Feb 2009 09:06:19 +0000
Subject: [PATCH] bug fix

---
 Robust/src/Benchmarks/Performance/Dispatch.java | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/Robust/src/Benchmarks/Performance/Dispatch.java b/Robust/src/Benchmarks/Performance/Dispatch.java
index b3fe20fc..80206913 100644
--- a/Robust/src/Benchmarks/Performance/Dispatch.java
+++ b/Robust/src/Benchmarks/Performance/Dispatch.java
@@ -1,10 +1,10 @@
 task start(StartupObject s {initialstate}) {
-    Foo f=new Foo(){run};
-    
+    Dispatch f=new Dispatch(){run};
+   
     taskexit(s{!initialstate});
 }
 
-task DoOperation(Foo f{run}) {
+task DoOperation(Dispatch f{run}) {
     if (f.count==1000000)
 	taskexit(f{!run});
     else {
@@ -13,9 +13,9 @@ task DoOperation(Foo f{run}) {
     }
 }
 
-public class Foo {
+public class Dispatch {
     flag run;
     int count;
-    public Foo() {
+    public Dispatch() {
     }
 }
\ No newline at end of file
-- 
2.34.1