-------- Forwarded Message -------- Subject: Libraries and text files Date: Sat, 16 May 2020 14:32:08 +0200 (CEST) From: fl To: Megill Norman
Hi Norm, Can you post this: Many softwares permit to open two kinds of files. Editors for instance. Especially Emacs. You can open libraries (well the received word is "load" ) and you can open text files. And both have their utility. Here we are in the same case. By the way if somebody could remove the header in the mmj2 files. Nobody uses it in my opinion. Since all that is under git, you might create a feature branch where the header is kept and remove it from the trunk. It would be possible to reintroduce the feature when it is complete and if it turns out it is useful. -- FL -- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/8241b3f0-fffc-4f6c-ba2e-8880df95c725%40googlegroups.com.
