From a33c64b45f54404c50741f04137c62fbe5c4efe2 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 --- 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 41c8152c75..88a2fe479b 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$"]