From be6324e183dd5d0e1411cf310588ebb47f0cf65f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 5 Oct 2018 14:19:38 -0700 Subject: [PATCH] chore(util/list_ref): missing include --- src/util/list_ref.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/util/list_ref.h b/src/util/list_ref.h index 0826d8938f..7a9c5a2ec1 100644 --- a/src/util/list_ref.h +++ b/src/util/list_ref.h @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include "util/buffer.h" #include "util/object_ref.h" namespace lean {