diff --git a/bin/lean-gdb.py b/bin/lean-gdb.py index a093a87090..6a8283af83 100644 --- a/bin/lean-gdb.py +++ b/bin/lean-gdb.py @@ -16,9 +16,9 @@ class LeanNamePrinter: return s if not self.val['m_ptr']: - return "lean::name()" + return "" else: - return 'lean::name(%s)' % rec(self.val['m_ptr'].dereference()) + return rec(self.val['m_ptr'].dereference()) class LeanListPrinter: """Print a lean::list object."""