diff --git a/scribble-lib/scribble/latex-render.rkt b/scribble-lib/scribble/latex-render.rkt index 289232ec..844ec771 100644 --- a/scribble-lib/scribble/latex-render.rkt +++ b/scribble-lib/scribble/latex-render.rkt @@ -1149,8 +1149,8 @@ [(#\ł) "{\\l}"] [(#\Ł) "{\\L}"] [(#\uA7) "{\\S}"] - [(#\〚) "$[\\![$"] - [(#\〛) "$]\\!]$"] + [(#\⟦ #\〚) "$[\\![$"] + [(#\⟧ #\〛) "$]\\!]$"] [(#\↦) "$\\mapsto$"] [(#\⊤) "$\\top$"] [(#\¥) "{\\textyen}"]