diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index 3861635a40..c65787b7c5 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -2161,7 +2161,7 @@ extern "C" LEAN_EXPORT object * lean_dbg_sleep(uint32 ms, obj_arg fn) { } extern "C" LEAN_EXPORT object * lean_dbg_trace_if_shared(obj_arg s, obj_arg a) { - if (lean_is_shared(a)) { + if (!lean_is_scalar(a) && lean_is_shared(a)) { io_eprintln(mk_string(std::string("shared RC ") + lean_string_cstr(s))); } return a;