another Scribble unicode->latex hack

svn: r16027
2009-09-16 22:42:55 +00:00 · 2009-09-16 22:42:55 +00:00 · 1b20b17dbe
commit 1b20b17dbe
parent 7273020b16
1 changed files with 2 additions and 0 deletions
--- a/collects/scribble/latex-render.ss
+++ b/collects/scribble/latex-render.ss
@ -763,6 +763,8 @@
                            [(#\ø) "{\\o}"]
                            [(#\Ø) "{\\O}"]
                            [(#\uA7) "{\\S}"]
+                            [(#\〚) "$[\\![$"]
+                            [(#\〛) "$]\\!]$"]
                            [else c])
                          c)])))
                (loop (add1 i)))))))