From ffacf702309dea0e86510b02a1c748781dc4090b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 20 Nov 2015 08:20:29 -0800 Subject: [PATCH] chore(library/io_state_stream): remove unused variable --- src/library/io_state_stream.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/library/io_state_stream.cpp b/src/library/io_state_stream.cpp index 9c00e2106..68884b8d2 100644 --- a/src/library/io_state_stream.cpp +++ b/src/library/io_state_stream.cpp @@ -15,7 +15,6 @@ io_state_stream const & operator<<(io_state_stream const & out, endl_class) { } io_state_stream const & operator<<(io_state_stream const & out, expr_kind const & k) { - options const & opts = out.get_options(); out.get_stream() << k; return out; }