addition to predefined virtuals

+ one character added

diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index 88f58f4eadb2e03fd7aa25ce751d8824dd67b303..d594924897662fbb462b25aafa505a3988358fa8 100644 (file)
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1512,7 +1512,7 @@ let predefined_classes = [
  ["?"; "¿"; "⸮"; ];
  [":"; "⁝"; ];
  ["."; "•"; "◦"; ];
- ["#"; "♯"; "⋕"; "⧣"; "⧤"; "⌘"; ];
+ ["#"; "â\99¯"; "â\8b\95"; "⧣"; "⧤"; "â\99®"; "â\8c\98"; ];
  ["+"; "⨭"; "⨮"; "⨁"; "⊕"; "⊞"; ];
  ["-"; "÷"; "⊢"; "⊩"; "⧟"; "⊟"; ];
  ["="; "≝"; "≡"; "≘"; "⊜"; "≗"; "≐"; "≑"; "≛"; "≚"; "≙"; "⌆"; "⧦"; "≋"; "⩳"; "≅"; "⩬"; "≂"; "≃"; "≈"; ];