max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(lean-gdb): do not print the u in u"limb" in python 2

Browse source
This commit is contained in:
Gabriel Ebner 2016-11-07 12:25:44 -05:00 • committed by Leonardo de Moura
parent 7da0acc3fd
commit d4fdea6751
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
bin/lean-gdb.py
View file

@ -9,7 +9,7 @@ class LeanNamePrinter:
def to_string(self):
def rec(imp):
s = repr(imp['m_str'].string()) if imp['m_is_string'] else str(imp['m_k'])
s = ("'%s'" % imp['m_str'].string()) if imp['m_is_string'] else str(imp['m_k'])
if imp['m_prefix']:
return "%s.%s" % (rec(imp['m_prefix'].dereference()), s)
else: