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)
commitd5a0491c811d7e7558c0f7b14c805d804721c854
tree2193a07dbedc419004e3ecb108ba67a6fbea8b9a
parentd48f193d11b4d4dca2675646ad76147f2d4765f2
parent9c9ba0b83a712e22f4ccb36c50ef9ae2642a02d7
Merge pull request #1457 from antonio-nino-diaz-arm/an/maintainers

maintainers: Modify format of file