From 981e35b6da09052b36ccd1be09a22b751111c71b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 8 Jan 2020 20:58:12 -0800
Subject: [PATCH] chore: style

---
 src/runtime/io.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp
index d1c279ec7b..8a1c5860dc 100644
--- a/src/runtime/io.cpp
+++ b/src/runtime/io.cpp
@@ -355,7 +355,7 @@ extern "C" obj_res lean_io_ref_swap(b_obj_arg ref, obj_arg a, obj_arg) {
 }
 
 extern "C" obj_res lean_io_ref_ptr_eq(b_obj_arg ref1, b_obj_arg ref2, obj_arg) {
-    // TODO: ref_maybe_mt
+    // TODO(Leo): ref_maybe_mt
     bool r = ref1 == ref2; // lean_to_ref(ref1)->m_value == lean_to_ref(ref2)->m_value;
     return set_io_result(box(r));
 }