metamath / metamath-exe

Metamath program - source code for the Metamath executable
GNU General Public License v2.0
75 stars 25 forks source link

Misc #124

Closed benjub closed 1 year ago

benjub commented 1 year ago

I'm not sure what this is: there were four "form feed" characters, each on its own line. They do not appear on github, so the diff looks empty.

digama0 commented 1 year ago

That sounds like \r\n newlines, which are the standard on windows. Git normalizes line endings to \n inside the repo and converts back and forth transparently when you use it on windows, but if you check in a file with \r\n newlines while the config flag for this behavior is disabled you can get \r\n in the repo files, which results in weird results on non-windows systems.

EDIT: Actually I guess it's \f not \r, which is much rarer. The only clue I could find (from https://www.asciihex.com/character/control/12/0x0C/ff-form-feed) is that it might be used by some printers for page breaking and is used conventionally in some plain text printable files, like this license.

On printers form feed load the next page. In many programming languages it is treated as whitespace, this way may be used to split logical divisions in code. In some terminal emulators it clears up the screen. Even nowadays it still can be find in some common simple text files in the role of page break character, such as the RFCs published by IETF.

benjub commented 1 year ago

Yes, it's form feeds. Displayed as ^L on my terminal and something like $F_F$ (the unicode version) in VS Code (see https://en.wikipedia.org/wiki/ASCII#Control_code_chart).

I unexpectedly found those because it messes up some regex searches.

digama0 commented 1 year ago

Tabs in makefiles are a part of the syntax, you can't change those. For LICENSE.TXT I think it's fine as long as we don't change the text, so if you want to remove the \f we can do that. On the other hand it might make it easier for automated tools to recognize the license if we don't mess with it; github seems to be fine with it so far.

benjub commented 1 year ago

@digama0 : I copied the license verbatim from https://www.gnu.org/licenses/old-licenses/gpl-2.0.txt (I do not know if it is worth using https://www.gnu.org/licenses/gpl-3.0.txt instead)

digama0 commented 1 year ago

GPLv2 vs v3 is a big debate in certain circles, so I would not make any modifications without more careful consideration.

jkingdon commented 1 year ago

The only clue I could find (from https://www.asciihex.com/character/control/12/0x0C/ff-form-feed) is that it might be used by some printers for page breaking and is used conventionally in some plain text printable files, like this license.

That's about right. People would use a form feed to delineate parts of a file (sort of like a section heading or something).

Even in the day I think this was somewhat rare, but today there is no reason to preserve it.