Merge pull request #1442 from jeenu-arm/sdei-dispatch-fix
authorDimitris Papastamos <dimitris.papastamos@arm.com>
Fri, 22 Jun 2018 10:38:12 +0000 (11:38 +0100)
committerGitHub <noreply@github.com>
Fri, 22 Jun 2018 10:38:12 +0000 (11:38 +0100)
SDEI: Fix dispatch bug


Trivial merge