This PR changes Lake to not set `LEAN_GITHASH` when in core (i.e. `bootstrap = true`). This avoids Lake rebuilding modules when the Lake watchdog is on one build of Lean/Lake and the command line is on a different one. |
||
|---|---|---|
| .. | ||
| src | ||
| stdlib | ||
This PR changes Lake to not set `LEAN_GITHASH` when in core (i.e. `bootstrap = true`). This avoids Lake rebuilding modules when the Lake watchdog is on one build of Lean/Lake and the command line is on a different one. |
||
|---|---|---|
| .. | ||
| src | ||
| stdlib | ||