Skip to content

Commit

Permalink
docs(elan): Remove reference to nightly Lean.
Browse files Browse the repository at this point in the history
  • Loading branch information
jcommelin committed Apr 13, 2019
1 parent 49c3a04 commit 7e06d60
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion docs/elan.md
Expand Up @@ -79,7 +79,7 @@ When you installed `elan`, it downloaded the latest stable release of Lean.
That may be too recent or too old for mathlib, and you really want mathlib.

1. Decide on a name for your package. We will use `my_playground`.
2. Run `leanpkg +nightly new my_playground`.
2. Run `leanpkg new my_playground`.
This will create a `my_playground` directory with a Lean project layout.
3. Run `cd my_playground`.
4. Run `leanpkg add leanprover/mathlib`.
Expand Down

0 comments on commit 7e06d60

Please sign in to comment.