Subject: bug#24302: TeX input method: wrong binding for \longrightarrow etc.

From: Andreas Abel <[email-masked]>
Date: Wed, 24 Aug 2016 20:43:11 +0200

See https://github.com/agda/agda/issues/1376

\longrightarrow should bind to

   character: ⟶ (displayed as ⟶) (codepoint 10230, #o23766, #x27f6)

However, it produces

   character: → (displayed as →) (codepoint 8594, #o20622, #x2192)

which is a short arrow.

I guess the other \long...arrow bindings should also be fixed.

Best,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

[email-masked]
http://www2.tcs.ifi.lmu.de/~abel/