diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-08-18 11:21:01 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-08-18 11:21:01 +0200 |
commit | d8dcf41334d7a6ff2d2eaa53f215c80ef26cd517 (patch) | |
tree | 58bca86cfcdda56ee85409c5b477202964d4fb12 /configure | |
parent | 576d65e2570d114c2e25ac2e25de29d3889af06f (diff) | |
download | compcert-d8dcf41334d7a6ff2d2eaa53f215c80ef26cd517.tar.gz compcert-d8dcf41334d7a6ff2d2eaa53f215c80ef26cd517.zip |
configure: Wording and formatting of the Skylake/OCaml warning
Diffstat (limited to 'configure')
-rwxr-xr-x | configure | 5 |
1 files changed, 3 insertions, 2 deletions
@@ -497,8 +497,9 @@ case "$ocaml_ver" in missingtools=true;; 4.02.*|4.03.*|4.04.*) echo "version $ocaml_ver -- good!" - echo "Some Intel processors of the Skylake and Kaby Lake generations have a hardware bug that this" - echo "version of OCaml runs into. To avoid this risk, it is recommended to use OCaml 4.05.";; + echo "WARNING: some Intel processors of the Skylake and Kaby Lake generations" + echo "have a hardware bug that can be triggered by this version of OCaml." + echo "To avoid this risk, it is recommended to use OCaml 4.05.";; 4.0*) echo "version $ocaml_ver -- good!";; ?.*) |