From d5e5b43e1f7afa43b91c24df1fb17a66446f304b Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 10 Dec 2019 23:20:39 -0600 Subject: [PATCH] fix shims for arrays --- src/core/mkshims.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/core/mkshims.ml b/src/core/mkshims.ml index ba9fb11c..33afafa1 100644 --- a/src/core/mkshims.ml +++ b/src/core/mkshims.ml @@ -80,7 +80,7 @@ let shims_array_pre_406 = " type 'a t = 'a array " -let shims_array_pre_408 = " +let shims_array_406_408 = " include Array type 'a t = 'a array " @@ -146,7 +146,7 @@ let () = write_file "CCShimsList_.ml" (if (major, minor) >= (4,8) then shims_list_post_408 else shims_list_pre_408); write_file "CCShimsArray_.ml" (if (major, minor) >= (4,8) then shims_array_post_408 - else if (major, minor) >= (4,6) then shims_fmt_pre_408 + else if (major, minor) >= (4,6) then shims_array_406_408 else shims_array_pre_406); write_file "CCShimsFormat_.ml" (if (major, minor) >= (4,8) then shims_fmt_post_408 else shims_fmt_pre_408); write_file "CCShimsFun_.ml" (if (major, minor) >= (4,8) then shims_fun_post_408 else shims_fun_pre_408);