Merge pull request #1527 from jts-arm/docs
authorDimitris Papastamos <[email protected]>
Fri, 17 Aug 2018 08:51:19 +0000 (09:51 +0100)
committerGitHub <[email protected]>
Fri, 17 Aug 2018 08:51:19 +0000 (09:51 +0100)
Fix typo in documentation page title


Trivial merge