commit | 55f3bc2d06032b3898ded7d4122a96355409d230 | [log] [tgz] |
---|---|---|
author | Dimitris Papastamos <dimitris.papastamos@arm.com> | Fri Aug 17 09:51:19 2018 +0100 |
committer | GitHub <noreply@github.com> | Fri Aug 17 09:51:19 2018 +0100 |
tree | da0f74f11af541f11576145d71d9a4c0657929ad | |
parent | b73b60e554a40be14da24771656d03d8c2b7dde3 [diff] | |
parent | ef9b68e2751547c28bb7696ed0c047e74f5e8f54 [diff] |
Merge pull request #1527 from jts-arm/docs Fix typo in documentation page title