doc-gen4: Add custom source linker support for HTML output

Stream: lean4

[Nicolas Rouquette]

Here's a small PR for a small but useful feature improvement for doc-gen4:
https://github.com/leanprover/doc-gen4/pull/341

[Henrik Böving]

Merged!

[Nicolas Rouquette]

Thanks @Henrik Böving

[Filippo A. E. Nuccio]

I've followed all the instructions at
https://github.com/leanprover/doc-gen4
and I've got a running local documentation. I've pushed it to a repo, but I cannot understand what the remote url for the doc is.

[Nicolas Rouquette]

@Filippo A. E. Nuccio

1) Have you pushed the generated doc to a pages branch so that the git server will properly serve the generated html pages?

See: https://docs.github.com/en/pages

2) Have you set the DOCGEN_SRC environment variable?

Note that the tool supports three options as described here:
https://github.com/leanprover/doc-gen4?tab=readme-ov-file#source-locations

[Filippo A. E. Nuccio]

Thanks, solved!