Merge pull request #1552 from glneo/build-fix
authorDimitris Papastamos <dimitris.papastamos@arm.com>
Fri, 31 Aug 2018 13:24:27 +0000 (14:24 +0100)
committerGitHub <noreply@github.com>
Fri, 31 Aug 2018 13:24:27 +0000 (14:24 +0100)
GIC: Fix build error


Trivial merge