You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: doc/dev/index.md
+1-1Lines changed: 1 addition & 1 deletion
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -8,7 +8,7 @@ You should not edit the `stage0` directory except using the commands described i
8
8
9
9
## Development Setup
10
10
11
-
You can use any of the [supported editors](../setup.md) for editing the Lean source code.
11
+
You can use any of the [supported editors](https://docs.lean-lang.org/lean4/doc/setup.html#editing) for editing the Lean source code.
12
12
If you set up `elan` as below, opening `src/` as a *workspace folder* should ensure that stage 0 (i.e. the stage that first compiles `src/`) will be used for files in that directory.
0 commit comments