From 8f6f1dc385f191f8e24d47944477dfa5c56f12ba Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Georges=20Dup=C3=A9ron?= Date: Thu, 1 Jun 2017 19:51:45 +0200 Subject: [PATCH] Added a few unicode characters --- unicode-chars.sty.rkt | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/unicode-chars.sty.rkt b/unicode-chars.sty.rkt index dc189269..2aa38445 100644 --- a/unicode-chars.sty.rkt +++ b/unicode-chars.sty.rkt @@ -245,5 +245,10 @@ \DeclareUnicodeCharacter{1D4CF}{\ensuremath{\mathcal{z}}}% 𝓏 \DeclareUnicodeCharacter{220C}{\ensuremath{\not\ni}}% ∌ \DeclareUnicodeCharacter{220B}{\ensuremath{\ni}}% ∋ +\DeclareUnicodeCharacter{2008}{\,}% Punctuation space +\DeclareUnicodeCharacter{2032}{\ensuremath{'}}% ′ (Prime) +\DeclareUnicodeCharacter{2033}{\ensuremath{''}}% ″ (2x Prime) +\DeclareUnicodeCharacter{2034}{\ensuremath{'''}}% ‴ (3x Prime) +\DeclareUnicodeCharacter{2057}{\ensuremath{''''}}% ⁗ (4x Prime) \makeatother }>>>|) \ No newline at end of file