From c636c87e4d1b3f11acc48118def4355093b4da65 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Sun, 4 Oct 2015 15:51:27 +0100
Subject: [PATCH] Eliminated unused variable

---
 src/test/old_interval.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/test/old_interval.cpp b/src/test/old_interval.cpp
index 91096a629..92064c03e 100644
--- a/src/test/old_interval.cpp
+++ b/src/test/old_interval.cpp
@@ -172,7 +172,6 @@ public:
 
 static void tst2() {
     typedef basic_interval_manager<unsynch_mpz_manager, false> mpzi_manager;
-    typedef mpzi_manager::interval mpzi;
     typedef mpzi_manager::scoped_interval scoped_mpzi;
 
     unsynch_mpz_manager nm;