Skip to content

Commit

Permalink
chore: add newline at end of file for lake new templates (#6026)
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
alissa-tung authored Nov 13, 2024
1 parent f08805e commit d5adadc
Showing 1 changed file with 4 additions and 2 deletions.
6 changes: 4 additions & 2 deletions src/lake/Lake/CLI/Init.lean
Original file line number Diff line number Diff line change
Expand Up @@ -24,12 +24,14 @@ s!"/{defaultLakeDir}
"

def basicFileContents :=
s!"def hello := \"world\""
s!"def hello := \"world\"
"

def libRootFileContents (libName : String) (libRoot : Name) :=
s!"-- This module serves as the root of the `{libName}` library.
-- Import modules here that should be built as part of the library.
import {libRoot}.Basic"
import {libRoot}.Basic
"

def mainFileName : FilePath :=
s!"{defaultExeRoot}.lean"
Expand Down

0 comments on commit d5adadc

Please sign in to comment.