Damien George 37d5aa1377 docs: Make the short port names in the port/version sidebar lowercase. ...

To make it neater and simpler.

2016-04-28 12:34:59 +01:00

..

layout.html

docs: Make index link point to "index.html" irrespective of port.

2015-06-27 13:41:24 +01:00

versions.html

docs: Make the short port names in the port/version sidebar lowercase.

2016-04-28 12:34:59 +01:00