diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.ott | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/language/l2.ott b/language/l2.ott index 8cbacf0d..b6a1396f 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -837,6 +837,8 @@ defs :: '' ::= | def1 .. defn :: :: Defs + + terminals :: '' ::= | ** :: :: starstar {{ tex \ensuremath{\mathop{\mathord{*}\mathord{*} } } }} |