From 38ee100117452ea707ea16e4523bab67dc1cd118 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 7 Nov 2016 14:21:39 -0500 Subject: [PATCH] chore(bin/lean-gdb): remove lean::name from string output --- bin/lean-gdb.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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."""