michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(library/io_state_stream): remove unused variable

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-20 08:20:29 -08:00
parent 628608ca7d
commit ffacf70230
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/library/io_state_stream.cpp
View file

@ -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) { io_state_stream const & operator<<(io_state_stream const & out, expr_kind const & k) {
options const & opts = out.get_options();
out.get_stream() << k; out.get_stream() << k;
return out; return out;
} }