javascript: fixed times-operator in names
commit2729962e0e682d5a95a8eef9ce68849853f3a553
authorraichoo <raichoo@googlemail.com>
dateMon 14 Jan 2013, 23:31 (14 years ago)
parent22ce6bf
src/IRTS/CodegenJavaScript.hs+1
@@ -122,6 +122,7 @@ translateIdentifier =
122122 replaceBadChars ':' = "__colon__"
123123 replaceBadChars '+' = "__plus__"
124124 replaceBadChars '-' = "__minus__"
125+ replaceBadChars '*' = "__times__"
125126 replaceBadChars '<' = "__lt__"
126127 replaceBadChars '>' = "__gt__"
127128 replaceBadChars '=' = "__eq__"