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)
commitdbd0bcfe008c08a7377e28d947d5354846cdc349
treef32e09ed8c16f4d60da7100c9bdef0dd5cfae1bb
parent64503b2f81bbd12051d8e0fd065a5a0b0c38bd2a
parent73308618fee8afc4518c592956b31864e57e48e7
Merge pull request #1848 from antonio-nino-diaz-arm/an/docs

Minor changes to documentation and comments