bug fixes
[IRC.git] / Robust / src / IR / ClassDescriptor.java
index e218c79001e9624fee570f29c5333b6f9110cd0a..43923d0cff3830e103b83e33840300a2232723a0 100644 (file)
@@ -130,7 +130,7 @@ public class ClassDescriptor extends Descriptor {
   }
 
   public String getSafeSymbol() {
-    return safename.replace(".","___________");
+    return safename.replace(".","___________").replace("$","___DOLLAR___");
   }
 
   public String printTree(State state) {