Add link to docs to the Readme

@jung will make sure, that this link resolves to toc.html instead of index.html.

added 1 commit

• b71f6a09 - Add link to docs to the Readme

Compare with previous version

The link works now: https://plv.mpi-sws.org/coqdoc/stdpp/

@robbertkrebbers this awaits your review

(Apparently after moving std++ to the iris organization, notifications were disabled; hence I was not notified of this MR).

Having the link in the README is surely a good idea. I'm not too convinced that having it in the title is nice, but what's the alternative?

Following Iris, I suppose we could (also?) add:

An HTML version of the latest sources (with hyperlinks for easier navigation) is available at XXX.

Having the link in the README is surely a good idea. I'm not too convinced that having it in the title is nice, but what's the alternative?

Having them right below the title is common for libraries at least in the Rust community, consider for example:

• https://github.com/hsivonen/encoding_rs
• https://github.com/llogiq/bytecount
• https://github.com/rust-lang/regex

I can move it down into the line below if you prefer? I think the link should be very prominent, not hidden somewhere in the text.

Following that, I have also added it to the description of the repo in Gitlab, see https://gitlab.mpi-sws.org/iris/stdpp

I dislike showing the URL, there should be some more friendly text for the hyperlink.

Could you change it into something you do like?

What about this? https://gitlab.mpi-sws.org/FP/iris-coq

Not that I am a big fan of [coqdoc] as text, though... but "Click here for Coqdoc" also is somewhat odd.

Is there a Coqdoc icon? Having a clickable image would be nice :D

I don't think there is a coqdoc icon. For Iris, we could also directly add [website] [technical docs]

The project website has the technical docs quite prominently, so I just added a link to that.

Works for me.

So, I guess this one and https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/192 can both be merged?

mentioned in commit 149f5aa7

merged

I guess this one and https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/192 can both be merged?

Done