From a78611a42a6f084d126c173c2b2aa01040e8d660 Mon Sep 17 00:00:00 2001 From: Vesa Karvonen Date: Thu, 18 Apr 2024 06:55:21 +0300 Subject: [PATCH] Use `Obj.obj` rather than `Obj.magic` where appropriate Both are currently `"%identity"`, but the `Obj` API distinguishes between the two. --- src/padding.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/padding.ml b/src/padding.ml index b43ac36..e3255c3 100644 --- a/src/padding.ml +++ b/src/padding.ml @@ -12,14 +12,14 @@ let copy_as_padded (o : 'a) : 'a = let t = Obj.tag o in if Sys.word_size = 64 && t != Obj.double_array_tag then begin let n = Obj.new_block t padded_size in - Array.blit (Obj.magic o) 0 (Obj.magic n) 0 original_size; - Obj.magic n + Array.blit (Obj.obj o) 0 (Obj.obj n) 0 original_size; + Obj.obj n end - else Obj.magic o + else Obj.obj o end - else Obj.magic o + else Obj.obj o end - else Obj.magic o + else Obj.obj o let make_padded_array n x = let a = Array.make (n + num_padding_words) x in