Fix HTML output of \gg and \ll

This is a part of bug #9372. The remaining part (\ne) is not easy to fix,
since \ne is a predefined macro internally, so the HTML output is done for
the expanded macro, and we have no machinery to assign a HTML output to a
complete macro.

diff --git a/lib/symbols b/lib/symbols
index 29d1a75cc75ef88317622c5f866acd447216e785..b76d3bd4b239cc6155813c5612e305a6faf3315f 100644 (file)
--- a/lib/symbols
+++ b/lib/symbols
@@ -289,7 +289,7 @@ diamondsuit        cmsy        125 168 mathord  ♢
 heartsuit          cmsy        126 169 mathord  ♡
 spadesuit          cmsy        127 170 mathord  ♠
 # We define lyxnot as mathrel in order to have proper alignment
-lyxnot             cmsy         54  47 mathrel  ∖
+lyxnot             cmsy         54  47 mathrel  /
 iffont cmsy
 # 9mu = 0.5em which is the extra space added to relation operators
 \def\not{\lyxnot\kern-9mu}
@@ -375,8 +375,8 @@ subseteq           cmsy        181 205 mathrel  ⊆
 in                 cmsy         50 206 mathrel  ∈
 ni                 cmsy         51  39 mathrel  ∋
 owns               cmsy         51  39 mathrel  ∋
-gg                 cmsy        192   0 mathrel  >
-ll                 cmsy        191   0 mathrel  <
+gg                 cmsy        192   0 mathrel  ≫
+ll                 cmsy        191   0 mathrel  ≪
 leftrightarrow     cmsy         36 171 mathrel  ↔
 leftarrow          cmsy        195 172 mathrel  ←
 gets               cmsy        195 172 mathrel  ←