diff options
| author | Murphy Sünnenwold <git@murphy-in.space> | 2023-05-24 16:46:06 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2023-05-24 16:46:06 +0200 |
| commit | b9d03be9755dae7f439763d181ec0c55a1e4c3d6 (patch) | |
| tree | 6b7519cb7fb2dcf2b2f8ab0734944e046ca556ea /library/src | |
| parent | 6af94be34ad1cb657194c788c07681b28d87fbaf (diff) | |
add r.double.not (#1315)
Diffstat (limited to 'library/src')
| -rw-r--r-- | library/src/symbols/sym.rs | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/library/src/symbols/sym.rs b/library/src/symbols/sym.rs index b49704bb..410eff4f 100644 --- a/library/src/symbols/sym.rs +++ b/library/src/symbols/sym.rs @@ -720,6 +720,7 @@ pub(crate) const SYM: &[(&str, Symbol)] = symbols! { r: '⊢', r.long: '⟝', r.double: '⊨', + r.double.not: '⊭', l: '⊣', l.long: '⟞', l.short: '⫞', |