Skip to content

Commit 956c77d

Browse files
MrBrain295MrBrain295
authored
Rename Lean to Lean.lean
1 parent 5a1eae2 commit 956c77d

2 files changed

Lines changed: 1 addition & 1 deletion

File tree

‎l/Lean‎

Lines changed: 0 additions & 1 deletion
This file was deleted.

‎l/Lean.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
#print "Hello World"

0 commit comments

Comments
 (0)