commit | ee2c8780875986954bce373e0ae1fc1a25aad704 | [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 | fa249cbbcdc06b1deff79bfe374980b6a441ec2a [diff] | |
parent | 5d23cb8bfea5fcb924dcf8c6b89af6f0fbdd9ac7 [diff] |
Merge pull request #1527 from jts-arm/docs Fix typo in documentation page title