From 6e4f8f6dc7ab7cdc0d9d852f6786947d3c4513cc Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 22 Aug 2022 00:44:42 +0200
Subject: [PATCH] addition to predefined virtuals

+ one character added
---
 matita/matita/predefined_virtuals.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index 88f58f4ea..d59492489 100644
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1512,7 +1512,7 @@ let predefined_classes = [
  ["?"; "¿"; "⸮"; ];
  [":"; "⁝"; ];
  ["."; "•"; "◦"; ];
- ["#"; "♯"; "⋕"; "⧣"; "⧤"; "⌘"; ];
+ ["#"; "♯"; "⋕"; "⧣"; "⧤"; "♮"; "⌘"; ];
  ["+"; "⨭"; "⨮"; "⨁"; "⊕"; "⊞"; ];
  ["-"; "÷"; "⊢"; "⊩"; "⧟"; "⊟"; ];
  ["="; "≝"; "≡"; "≘"; "⊜"; "≗"; "≐"; "≑"; "≛"; "≚"; "≙"; "⌆"; "⧦"; "≋"; "⩳"; "≅"; "⩬"; "≂"; "≃"; "≈"; ];
-- 
2.39.2