From 38524475c93e46ed28c4e970d6367be270a17539 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 5 Aug 2016 17:22:01 -0700 Subject: [PATCH] chore(library/attribute_manager): fix warning --- src/library/attribute_manager.h | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/library/attribute_manager.h b/src/library/attribute_manager.h index 16afead72d..83f4d6a835 100644 --- a/src/library/attribute_manager.h +++ b/src/library/attribute_manager.h @@ -85,8 +85,9 @@ private: protected: virtual void write_entry(serializer &, attr_data const &) const override final {} virtual attr_data_ptr read_entry(deserializer &) const override final { return attr_data_ptr(new attr_data); } - virtual environment set_untyped(environment const & env, io_state const & ios, name const & n, attr_data_ptr data, - bool persistent) const override final { + virtual environment set_untyped(environment const & /*env */, io_state const & /* ios */, + name const & /* n */, attr_data_ptr /* data */, + bool /* persistent */) const override final { // TODO(sullrich): Use priority from `data` as soon as available lean_unreachable(); }