From 7213ff0065c239ceef801485f48a9bce002b9016 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Fri, 14 Jul 2023 01:39:54 +1000 Subject: [PATCH] doc: document generating releases via tags (#2302) --- doc/dev/index.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/doc/dev/index.md b/doc/dev/index.md index 55210b3d81..da0befd4fd 100644 --- a/doc/dev/index.md +++ b/doc/dev/index.md @@ -57,3 +57,10 @@ You might find that debugging through elan, e.g. via `gdb lean`, disables some things like symbol autocompletion because at first only the elan proxy binary is loaded. You can instead pass the explicit path to `bin/lean` in your build folder to gdb, or use `gdb $(elan which lean)`. + +It is also possible to generate releases that others can use, +simply by pushing a tag to your fork of the Lean 4 github repository +(and waiting about an hour; check the `Actions` tab for completion). +If you push `my-tag` to a fork in your github account `my_name`, +you can then put `my_name/lean4:my-tag` in your `lean-toolchain` file in a project using `lake`. +(You must use a tag name that does not start with a numeral, or contain `_`).