Should eliminate the GIF directories & just use Unicode? That is, for example, redirect all uses of <https://us.metamath.org/mpegif/> to <https://us.metamath.org/mpeuni/> ?
I welcome comments/thoughts. A few notes are below. --- David A. Wheeler === The Metamath project has, for many years, generated HTML pages with embedded GIF images. For a very long time this was the only practical way for most people to read the results. However, today practically all web browsing systems support Unicode. We switched to Unicode as the default years ago. Many people's fonts didn't cover math symbols, but when we posted web fonts (my fault :-) ) that problem was basically solved. At this point I think the primary reason to keep GIF directories is to make copying text easier: https://us.metamath.org/mpeuni/mmset.html#textonly That's a perfectly valid use case, as long as people are actually doing it. I don't know how many people find that useful. Generating everything twice takes time, but that's not a big deal. It does create more opportunities for error & complicates our scripts. The big advantage of eliminating the GIF generation would be to save disk space. Because we generate everything twice, we use about double the disk space. Anyone can see our current disk space status by viewing this page: https://us.metamath.org/status.txt The main drive /dev/sda has 26G, with 1.3G available (95% used). We can pay for more space, but there's a jump in price. We should be fine for a long time as long as we keep log files limited in size, but any error in its configuration can cause problems (as illustrated recently). There may be other issues I'm not aware of. -- 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/CBC0AA4D-F5ED-406C-A8B4-6E871072E1AA%40dwheeler.com.
