From ff455d3ec9c04960bdd06415529e9db57d9daecf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 6 Jan 2017 21:22:27 -0800 Subject: [PATCH] chore(library/vm/vm): warning --- src/library/vm/vm.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index c1729da287..2abfccbdaa 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -3144,6 +3144,7 @@ auto vm_state::profiler::get_snapshots() -> snapshots { return r; } +#if 0 static bool equal_fns(vm_state::profiler::snapshot const & s1, vm_state::profiler::snapshot const & s2) { if (s1.m_stack.size() != s2.m_stack.size()) return false; for (unsigned i = 0; i < s1.m_stack.size(); i++) { @@ -3152,6 +3153,7 @@ static bool equal_fns(vm_state::profiler::snapshot const & s1, vm_state::profile } return true; } +#endif void vm_state::profiler::snapshots::display(std::ostream & out) const { for (auto & cum_time : m_cum_times) {