From 9bd0e3e58c7b81c4b417892346555257c0e65ed9 Mon Sep 17 00:00:00 2001 From: Matthew Flatt Date: Fri, 18 Jul 2014 07:39:33 +0100 Subject: [PATCH] scribble: another Unicode mapping for Latex output This mapping is needed by the "redex-unstable" documentation. Merge to v6.1 (cherry picked from commit a33c64b45f54404c50741f04137c62fbe5c4efe2) --- pkgs/scribble-pkgs/scribble-lib/scribble/latex-render.rkt | 2 ++ 1 file changed, 2 insertions(+) diff --git a/pkgs/scribble-pkgs/scribble-lib/scribble/latex-render.rkt b/pkgs/scribble-pkgs/scribble-lib/scribble/latex-render.rkt index 090b03b421..2bb0240fba 100644 --- a/pkgs/scribble-pkgs/scribble-lib/scribble/latex-render.rkt +++ b/pkgs/scribble-pkgs/scribble-lib/scribble/latex-render.rkt @@ -1002,6 +1002,8 @@ [(#\”) "{''}"] [(#\u2013) "{--}"] [(#\u2014) "{---}"] + [(#\〈) "$\\langle$"] + [(#\〉) "$\\rangle$"] [(#\∞) "$\\infty$"] [(#\⇓) "$\\Downarrow$"] [(#\↖) "$\\nwarrow$"]