mybin

commit 23cbddbd78b108e2cd2bdcf07a13dfa2f7c48663
parent 8cb0bd2c86d5aaf75ba43720549ac6c406f23e15
Author: Antoine Amarilli <a3nm@a3nm.net>
Date:   Fri, 27 Sep 2013 17:14:51 +0200

fix for otherlanguage weirdness

Diffstat:
shorthand.pl
 | 
2
+-

1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/shorthand.pl b/shorthand.pl
@@ -172,7 +172,7 @@ while (<>) {
       }
     } else {
       if ($2 eq "=>") {
-        $key = "\$\\Rightarrow\$";
+        $key = "\\textcolor{red}{\$\\Rightarrow\$}";
       }
       $l = "$3";
     }