From d4fdea6751b99b2fe872715fb0d98473db9dfd08 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 7 Nov 2016 12:25:44 -0500
Subject: [PATCH] fix(lean-gdb): do not print the u in u"limb" in python 2

---
 bin/lean-gdb.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/bin/lean-gdb.py b/bin/lean-gdb.py
index 2bca84c545..b530c110d9 100644
--- a/bin/lean-gdb.py
+++ b/bin/lean-gdb.py
@@ -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: