Re: [Metamath] Re: Should eliminate the GIF directories & just use Unicode?

I don't think the redirect would be that difficult, it is a one time apache configuration thing, possibly plus updates to the mirrors. On Mon, Jan 2, 2023 at 11:25 PM Jim Kingdon wrote: > There are a lot of ideas on this thread which might be worth doing, but > the redirect from mpegif to

Re: [Metamath] Re: Should eliminate the GIF directories & just use Unicode?

There are a lot of ideas on this thread which might be worth doing, but the redirect from mpegif to mpeuni is the only which is in my mind a (likely) prerequisite for retiring mpegif. Most of the others we could do later if we find we wish we had them. On 1/2/23 07:49, Samiro Discher wrote:

Re: [Metamath] Should eliminate the GIF directories & just use Unicode?

I think it's not worth it to have ascii symbols in title attributes on every character. This will unnecessarily blow up the page size quite considerably. I think Benoit's suggestion of an all-ascii version of the pages is better - I think this is already implemented in one of the alternate

Re: [Metamath] Should eliminate the GIF directories & just use Unicode?

> On Jan 2, 2023, at 2:47 PM, Glauco wrote: > > 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? Yes. Any HTML element can have a "global attribute", and

[Metamath] Re: Should eliminate the GIF directories & just use Unicode?

I think that we should drop the GIF directories, to lighten maintenance, and that we should in place add an ascii version, https://us.metamath.org/mpeascii/, so that the feature mentioned by Glauco stay (and be even better). The ascii pages should not be hard to generate: in the metamath.c

[Metamath] Re: Should eliminate the GIF directories & just use Unicode?

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

[Metamath] Re: Should eliminate the GIF directories & just use Unicode?

Another issue that immediately comes to my mind is that in such case one shouldn't invalidate old hyperlinks, e.g. https://us.metamath.org/mpegif/id.html should be redirected to https://us.metamath.org/mpeuni/id.html in case the mpegif pages are removed. David A. Wheeler schrieb am Montag, 2.

[Metamath] Should eliminate the GIF directories & just use Unicode?

Should eliminate the GIF directories & just use Unicode? That is, for example, redirect all uses of to ? I welcome comments/thoughts. A few notes are below. --- David A. Wheeler === The Metamath project has, for many years,