change

diff --git a/Robust/src/Main/Main.java b/Robust/src/Main/Main.java
index ed7b5cf5f9c8f9299f4f85e511130edb6bf4d5fd..9eefae238d2a5af96974f13832542e5c97cd9ec4 100644 (file)
--- a/Robust/src/Main/Main.java
+++ b/Robust/src/Main/Main.java
@@ -219,6 +219,8 @@ public class Main {
        state.THREAD=true;
       else if (option.equals("-dsm"))
        state.DSM=true;
+      else if (option.equals("-recoverystats"))
+  state.DSMRECOVERYSTATS=true;
       else if (option.equals("-dsmtask"))
   state.DSMTASK=true;
       else if (option.equals("-singleTM"))
@@ -292,7 +294,7 @@ public class Main {
        sourcefiles.add(args[i]);
       }
     }
-
+    
     //add default classpath
     if (state.classpath.size()==1)
       state.classpath.add(ClassLibraryPrefix);