Skip to content
This repository has been archived by the owner on Aug 29, 2023. It is now read-only.

Commit

Permalink
Make leanproject new use latest mathlib-supported Lean.
Browse files Browse the repository at this point in the history
  • Loading branch information
PatrickMassot committed Mar 7, 2020
1 parent c3c9c3b commit 7f0216d
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions mathlibtools/lib.py
Original file line number Diff line number Diff line change
Expand Up @@ -392,6 +392,7 @@ def new(cls, path: Path = Path('.'), cache_url: str = '',
subprocess.run(['leanpkg', 'new', str(path)])

proj = cls.from_path(path, cache_url, force_download)
proj.lean_version = mathlib_lean_version()
proj.write_config()
proj.add_mathlib()
return proj
Expand Down

0 comments on commit 7f0216d

Please sign in to comment.