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

2023-01-02 Thread Mario Carneiro
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?

2023-01-02 Thread Jim Kingdon
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:

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

2023-01-02 Thread Benoit
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?

2023-01-02 Thread Glauco
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?

2023-01-02 Thread Samiro Discher
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.