newline at end of file

Stream: general

[Kevin Buzzard]

I just noticed that VS Code puts a newline at the end of a file when I hit Ctrl-S. Is this what mathlib wants? If not, can I turn this off? I just noticed that data/quot.lean has no newline at the end of the file.

[Wojciech Nawrocki]

This is due to POSIX: https://stackoverflow.com/a/729795 .

[Kevin Buzzard]

IANACS but are you saying that my PR is not going to be rejected because I added a new line at the end of data/quot.lean?

[Wojciech Nawrocki]

I suppose that is up to the reviewers, but generally having a newline at the end is standard behaviour on Linux (and maybe Mac), so it should be fine.

[Johan Commelin]

https://github.com/leanprover-community/mathlib/blob/master/.vscode/settings.json#L7

[Johan Commelin]

@Kevin Buzzard :up:

[Kevin Buzzard]

Got it. I was suddenly concerned that I was accidentally breaking with mathlib convention with today's PR, so I tried deleting the newline, and VS Code put it back :-)

[Johannes Hölzl]

I added this setting to reduce the amount of spuriously appearing / disappearing new lines.