Unclear error when running in a git repo without "origin" remote

[Ruben-VandeVelde]

doc-gen4 prints only

error: stderr:
uncaught exception: git exited with code 128

without any indication what's wrong. It's not clear to me it should require a git repo to build at all, but if it does, it should handle issues with its expectations more gracefully.

[hargoniX]

Fixed.

The reason it requires a git repo right now is for the source linking, I thought it was a reasonable assumption to make at the time that in general Lean code ends up on Github. That said I guess as the community grows different use cases will pop up that will need more handling in the source linker.