Merge pull request #1457 from antonio-nino-diaz-arm/an/maintainers
authorDimitris Papastamos <dimitris.papastamos@arm.com>
Thu, 28 Jun 2018 13:49:33 +0000 (14:49 +0100)
committerGitHub <noreply@github.com>
Thu, 28 Jun 2018 13:49:33 +0000 (14:49 +0100)
maintainers: Modify format of file


Trivial merge