From 3dd7a69068a1d8e4cd7f500f18d8ff792be1d382 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 2 Mar 2017 17:37:59 +0100 Subject: [PATCH] chore(bin/lean-gdb): fix mismatched type? --- 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 635efcc456..3bafdcd1a0 100644 --- a/bin/lean-gdb.py +++ b/bin/lean-gdb.py @@ -46,7 +46,7 @@ class LeanExprPrinter: def __init__(self, val): - self.kind = val['m_ptr']['m_kind'] + self.kind = int(val['m_ptr']['m_kind']) subtype = gdb.lookup_type(LeanExprPrinter.expr_kinds[self.kind][0]) self.val = val['m_ptr'].cast(subtype.pointer()).dereference()