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 `_`).