commit: d5adadc00ec0e1b36d691e3c124e133c096adcaa

[log]
author: Alissa Tung <alissa-tung@outlook.com>

Thu Nov 14 03:39:47 2024 +0800
committer: GitHub <noreply@github.com>

Wed Nov 13 19:39:47 2024 +0000
tree: 80b597a71d67e4ad4fe48643096537cf80213bfe
parent: f08805e5c446d0b7d7c61861ea035d1cdb82e944 [diff]

chore: add newline at end of file for `lake new` templates (#6026)

This PR adds a newline at end of each Lean file generated by `lake new`
templates.

I have tested it with a locally compiled Lean with this commit. I hope
these changes make `lake new`'s behavior more consistent with the Lean 4
plugins and libraries newlines convention.

src/lake/Lake/CLI/Init.lean[diff]

1 file changed

tree: 80b597a71d67e4ad4fe48643096537cf80213bfe

README.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean (documentation source: doc/make/index.md).