From 1c9e5226d80204e40181d4a6aacf937a69a49de3 Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Mon, 12 Aug 2013 14:52:36 -0700 Subject: [PATCH] Fix compile-error by adding "defined" to interval_def.h --- src/interval/interval_def.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/interval/interval_def.h b/src/interval/interval_def.h index 881b267a3..667749fd6 100644 --- a/src/interval/interval_def.h +++ b/src/interval/interval_def.h @@ -242,7 +242,7 @@ interval & interval::operator*=(interval const & o) { using std::swap; interval const & i1 = *this; interval const & i2 = o; -#if LEAN_DEBUG || LEAN_TRACE +#if defined(LEAN_DEBUG) || defined(LEAN_TRACE) bool i1_contains_zero = i1.contains_zero(); bool i2_contains_zero = i2.contains_zero(); #endif