Merge pull request #482 from sharkcz/aarch64
authorTom Tromey <tom@tromey.com>
Tue, 9 Apr 2019 20:00:10 +0000 (14:00 -0600)
committerGitHub <noreply@github.com>
Tue, 9 Apr 2019 20:00:10 +0000 (14:00 -0600)
fix check for Linux/aarch64


Trivial merge