Adding a font-awesome icon for external links

[panglesd]

This is a PR to address Issue #669.

It adds an icon after external links. The icon is taken from here: https://fontawesome.com/v6.0/icons/up-right-from-square (it's the only "external link" icon that is not a Pro icon):

I tried to follow both suggestions: making the svg inline in the css, and using currentColor. However, this is not that easy: one cannot manipulate the color of an svg pseudo-element that easily.
I came up with the following ugly hack solution: the svg is a mask, and the background color is currentColor.
This comes with a price: with both its prefix and unprefixed version, caniuse report that only 95.41% of users have a browser that supports this functionnality. To distinguish between desktop and mobile, its respectively 96.52% and 95.16%.
Here are some details:

• 0.73% as IE users
• 0.43% as old firefox versions (version before 53)
• 1.19% as "opera Mini" users (in fact, support is unknown, but I can't check!)
• 0.28% as "Android Browser" users
• 1.07% as "UC Browser for Internet" users

For those people, the filter won't work, so instead of the currentColor external link icon, they will have a currentColor filled square...

How acceptable do you think that is? If that's not acceptable, there are to options:

• Give up on currentColor. We can use the widely supported (99.95% for desktop) content property. The icon will always be black.
• Give up on inlining the svg in the css, adding the svg as an element (instead of a pseudo-element) and giving it the color currentColor.

[Julow]

Nice !

For those people, the filter won't work, so instead of the currentColor external link icon, they will have a currentColor filled square

That's fine to me. We also use CSS-variables and media queries which have a similar compatiblity: https://caniuse.com/css-variables
The fallback to a filled square is really nothing compared to the mess that would result from not having the other features we use.

[EmileTrotignon]

Could this be rebased @panglesd ?

[panglesd]

I don't think a mutual agreement was reached in #669, so I would be in favor of letting this PR rot. The feature is of pretty low priority/interest (but it was a good exercise to enter in this codebase!).

[panglesd]

Let's tidy the open PRs.

[Julow]

This contains two changes to the html generator:

• Add the external-link class to external links ("external" in the sense of a link to a page not generated by Odoc).
• Change the default CSS to show an icon on .external-links.

I think the first change should be merged so that documentation integrator can style these links differently if needed. There seem to be several people interested in this: #669

[panglesd]

That seems a fair compromise. I'll reopen the PR, rebase and remove the added css.

[panglesd]

I removed the added icon but kept the class on external links, and rebased.

Feel free to merge (or close) this PR!

[Julow]

A rebase is needed and the tests should be promoted on < 4.10.

This is harmless and improves customizability. Let's merge!