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

…

versions.html

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

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