commit | d5a0491c811d7e7558c0f7b14c805d804721c854 | [log] [tgz] |
---|---|---|
author | Dimitris Papastamos <dimitris.papastamos@arm.com> | Thu Jun 28 14:49:33 2018 +0100 |
committer | GitHub <noreply@github.com> | Thu Jun 28 14:49:33 2018 +0100 |
tree | 2193a07dbedc419004e3ecb108ba67a6fbea8b9a | |
parent | d48f193d11b4d4dca2675646ad76147f2d4765f2 [diff] | |
parent | 9c9ba0b83a712e22f4ccb36c50ef9ae2642a02d7 [diff] |
Merge pull request #1457 from antonio-nino-diaz-arm/an/maintainers maintainers: Modify format of file