diff options
| author | Tom Kelly <ctk21@cl.cam.ac.uk> | 2021-03-04 16:12:04 +0000 |
|---|---|---|
| committer | Tom Kelly <ctk21@cl.cam.ac.uk> | 2021-03-04 16:12:04 +0000 |
| commit | 56ef5a61ddfadf76dbfdfad14763486a1b0a7739 (patch) | |
| tree | e76415f2d9ddd91dcfc65588be29c0ec125c95c9 /tools | |
| parent | 4076a604e6e8d6e042209e0416c92d6317003a4b (diff) | |
| parent | e41dc9c44327f40c1ab0feea12f779c931c9e31e (diff) | |
| download | ocaml-56ef5a61ddfadf76dbfdfad14763486a1b0a7739.tar.gz | |
Merge commit 'e41dc9c44327f40c1ab0feea12f779c931c9e31e' into parallel_minor_gc_4_12
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/caml_tex.ml | 2 | ||||
| -rwxr-xr-x | tools/ci/inria/main | 3 |
2 files changed, 3 insertions, 2 deletions
diff --git a/tools/caml_tex.ml b/tools/caml_tex.ml index ae89477d9b..79fb3c28db 100644 --- a/tools/caml_tex.ml +++ b/tools/caml_tex.ml @@ -352,7 +352,7 @@ module Output = struct let catch_warning = function | [] -> None - | s :: _ when string_match ~!{|Warning \([0-9]+\):|} s 0 -> + | s :: _ when string_match ~!{|Warning \([0-9]+\)\( \[[a-z-]+\]\)?:|} s 0 -> Some (Warning (int_of_string @@ matched_group 1 s)) | _ -> None diff --git a/tools/ci/inria/main b/tools/ci/inria/main index ebed3e694b..30db36e9ae 100755 --- a/tools/ci/inria/main +++ b/tools/ci/inria/main @@ -226,7 +226,8 @@ export LC_ALL=C git clean -q -f -d -x if $flambda; then - confoptions="$confoptions --enable-flambda --enable-flambda-invariants" + confoptions="$confoptions --enable-flambda --enable-flambda-invariants \ +--disable-naked-pointers" fi eval ./configure "$CCOMP" $build $host --prefix='$instdir' $confoptions |