diff --git a/src/util/debug.h b/src/util/debug.h
index 6929e464d..881976d41 100644
--- a/src/util/debug.h
+++ b/src/util/debug.h
@@ -108,7 +108,8 @@ public:
 };
 namespace debug {
 template<typename T> void display_var(char const * name, T const & value) {
-    std::cerr << name << " : " << typeid(value).name() << " := "
+    // commented typeid(value).name() since the name is mangled
+    std::cerr << name << /* " : " << typeid(value).name() << */ " := "
               << std::boolalpha << value << std::noboolalpha
               << std::endl; }
 }