Merge pull request #1442 from jeenu-arm/sdei-dispatch-fix
authorDimitris Papastamos <[email protected]>
Fri, 22 Jun 2018 10:38:12 +0000 (11:38 +0100)
committerGitHub <[email protected]>
Fri, 22 Jun 2018 10:38:12 +0000 (11:38 +0100)
SDEI: Fix dispatch bug


Trivial merge