From: Matthijs Kooijman Date: Tue, 24 Nov 2009 15:45:39 +0000 (+0100) Subject: Use the unicode rightwards arrow instead of \rightarrow. X-Git-Tag: final-thesis~141 X-Git-Url: https://git.stderr.nl/gitweb?a=commitdiff_plain;h=0726312509c9a708eb4ecc0ac36b6b67eba45ad5;p=matthijs%2Fmaster-project%2Freport.git Use the unicode rightwards arrow instead of \rightarrow. It seems this uses the arrow from the current font instead of something else, which looks slightly better. --- diff --git a/pret-lam.lua b/pret-lam.lua index 1f073f8..97a5376 100644 --- a/pret-lam.lua +++ b/pret-lam.lua @@ -21,7 +21,7 @@ local symbols = { -- (U+00A0). [' '] = {repr = ' '}, ['_'] = {repr = '\\_'}, - ['->'] = {repr = '\\rightarrow'}, + ['->'] = {repr = '→'}, ['=>'] = {repr = '⇒'}, -- The default * sits very high above the baseline, \ast (u+2217) looks -- better.