Merge pull request #1848 from antonio-nino-diaz-arm/an/docs
authorAntonio Niño Díaz <antonio.ninodiaz@arm.com>
Fri, 1 Mar 2019 09:16:58 +0000 (09:16 +0000)
committerGitHub <noreply@github.com>
Fri, 1 Mar 2019 09:16:58 +0000 (09:16 +0000)
Minor changes to documentation and comments


Trivial merge