max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(util/rb_tree): suppress warning from suppressing unknown warning

Browse source
This commit is contained in:
Sebastian Ullrich 2019-03-21 17:45:49 +01:00 • committed by Leonardo de Moura
parent cf72e97455
commit fc40fbb93f
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/util/rb_tree.h
View file

@ -5,7 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#if !defined(__has_warning) || __has_warning("-Wreturn-std-move")
#pragma clang diagnostic ignored "-Wreturn-std-move"
#endif
#include <utility>
#include <algorithm>
#include "runtime/optional.h"