From 6785ad98444fe85be67bae14fa69c3cf672296bb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 14 Feb 2019 15:21:53 -0800
Subject: [PATCH] fix(library/init/lean/default): missing file

---
 library/init/lean/default.lean | 1 +
 src/boot/init/lean/default.cpp | 8 +++++---
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/library/init/lean/default.lean b/library/init/lean/default.lean
index 5c0848a73a..d4994c0035 100644
--- a/library/init/lean/default.lean
+++ b/library/init/lean/default.lean
@@ -6,3 +6,4 @@ Authors: Leonardo de Moura
 prelude
 import init.lean.compiler
 import init.lean.frontend
+import init.lean.extern
diff --git a/src/boot/init/lean/default.cpp b/src/boot/init/lean/default.cpp
index 0fd3efad10..762d38f788 100644
--- a/src/boot/init/lean/default.cpp
+++ b/src/boot/init/lean/default.cpp
@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: init.lean.default
-// Imports: init.lean.compiler.default init.lean.elaborator
+// Imports: init.lean.compiler.default init.lean.frontend init.lean.extern
 #include "runtime/object.h"
 #include "runtime/apply.h"
 typedef lean::object obj;    typedef lean::usize  usize;
@@ -15,11 +15,13 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64;
 #pragma GCC diagnostic ignored "-Wunused-but-set-variable"
 #endif
 void initialize_init_lean_compiler_default();
-void initialize_init_lean_elaborator();
+void initialize_init_lean_frontend();
+void initialize_init_lean_extern();
 static bool _G_initialized = false;
 void initialize_init_lean_default() {
  if (_G_initialized) return;
  _G_initialized = true;
  initialize_init_lean_compiler_default();
- initialize_init_lean_elaborator();
+ initialize_init_lean_frontend();
+ initialize_init_lean_extern();
 }