Merge pull request #725 from jeenu-arm/fix-duplicate-title
authordanh-arm <dan.handley@arm.com>
Wed, 12 Oct 2016 10:13:58 +0000 (11:13 +0100)
committerGitHub <noreply@github.com>
Wed, 12 Oct 2016 10:13:58 +0000 (11:13 +0100)
Docs: Rename duplicate title in porting guide


Trivial merge