From 10122ba38b5cd9ff72e0425f561f0a1d174e6e5b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 20 Jul 2021 09:14:50 -0700 Subject: [PATCH] chore: try to fix compilation error at CI --- src/runtime/object.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index 6dec94b734..675db589fa 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -74,7 +74,7 @@ extern "C" void lean_inc_ref_cold(lean_object * o) { } extern "C" void lean_inc_ref_n_cold(lean_object * o, unsigned n) { - std::atomic_fetch_sub_explicit(lean_get_rc_mt_addr(o), n, std::memory_order_relaxed); + std::atomic_fetch_sub_explicit(lean_get_rc_mt_addr(o), (int)n, std::memory_order_relaxed); } extern "C" size_t lean_object_byte_size(lean_object * o) {