The gif version has a useful feature: when you hover on a symbol, the ascii string for the symbol is shown.
Would it be possible to have the same behavior in the Unicode version? -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f01c9ac8-22f5-4354-92c3-341c08a97483n%40googlegroups.com.
