diff options
| author | Jack Lloyd <[email protected]> | 2018-11-09 16:08:09 -0500 |
|---|---|---|
| committer | Jack Lloyd <[email protected]> | 2018-11-09 16:08:09 -0500 |
| commit | 7d2ae571d3e83b936b4fc401b58eaa5b353bf01a (patch) | |
| tree | f65c1d91b33ed19231fc0d1d437099645f4925b9 | |
| parent | 99050e91c4373594f74f2e40f9cd4897aacc0026 (diff) | |
Add --disable-bmi2, --disable-rdseed, --disable-rdrand flags
GH #1721 #1718
| -rwxr-xr-x | configure.py | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/configure.py b/configure.py index b6cba2d19..d28945d0c 100755 --- a/configure.py +++ b/configure.py @@ -336,7 +336,7 @@ def process_command_line(args): # pylint: disable=too-many-locals,too-many-state help='specify OS features to disable') isa_extensions = [ - 'SSE2', 'SSSE3', 'SSE4.1', 'SSE4.2', 'AVX2', + 'SSE2', 'SSSE3', 'SSE4.1', 'SSE4.2', 'AVX2', 'BMI2', 'RDRAND', 'RDSEED', 'AES-NI', 'SHA-NI', 'AltiVec', 'NEON', 'ARMv8Crypto'] |