From 8e8232605a37f346b56cf65026cb85b9f74b138e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 27 Mar 2018 10:45:47 -0700 Subject: [PATCH] chore(library/compiler/inliner): fix weird include --- src/library/compiler/inliner.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/compiler/inliner.cpp b/src/library/compiler/inliner.cpp index a063d7c180..73b909b7bb 100644 --- a/src/library/compiler/inliner.cpp +++ b/src/library/compiler/inliner.cpp @@ -5,12 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include #include "kernel/inductive/inductive.h" #include "library/util.h" #include "library/module.h" #include "library/trace.h" #include "library/normalize.h" +#include "library/attribute_manager.h" #include "library/vm/vm.h" #include "library/compiler/util.h" #include "library/compiler/compiler_step_visitor.h"