diff --git a/Lake/Package.lean b/Lake/Package.lean
index 97ae0df9e8..73ccc77ba0 100644
--- a/Lake/Package.lean
+++ b/Lake/Package.lean
@@ -286,6 +286,18 @@ structure PackageConfig extends WorkspaceConfig where
   -/
   moreLibTargets : Array FileTarget := #[]
 
+  /--
+    Whether to expose symbols within the executable to the Lean interpreter.
+    This allows the executable to interpret Lean files (e.g.,  via
+    `Lean.Elab.runFrontend`).
+
+    Implementation-wise, this passes `-rdynamic` to the linker when building
+    on non-Windows systems.
+
+    Defaults to `false`.
+  -/
+  supportInterpreter : Bool := false
+
   /--
     Additional arguments to pass to `leanc`
       while compiling the package's binary executable.
@@ -476,9 +488,16 @@ def binFile (self : Package) : FilePath :=
 def moreLibTargets (self : Package) : Array FileTarget :=
   self.config.moreLibTargets
 
-/-- The package's `moreLinkArgs` configuration. -/
+/-- The package's `supportInterpreter` configuration. -/
+def supportInterpreter (self : Package) : Bool :=
+  self.config.supportInterpreter
+
+/-- `-rdynamic` (if non-Windows and `supportInterpreter`) plus `moreLinkArgs` -/
 def moreLinkArgs (self : Package) : Array String :=
-  self.config.moreLinkArgs
+  if self.supportInterpreter && !Platform.isWindows then
+    #["-rdynamic"] ++ self.config.moreLinkArgs
+  else
+    self.config.moreLinkArgs
 
 /-- Whether the given module is in the package. -/
 def hasModule (mod : Name) (self : Package) : Bool :=
diff --git a/README.md b/README.md
index 4d622f8879..5d6c530c4e 100644
--- a/README.md
+++ b/README.md
@@ -116,6 +116,7 @@ Workspace options are shared across a package and its dependencies.
 * `binDir`: The build subdirectory to which Lake should output the package's binary executable. Defaults to `bin`.
 * `binRoot`: The root module of the package's binary executable. Defaults to `Main`. The root is built by recursively building its local imports (i.e., fellow modules of the package). This setting is most useful for packages that are distributing both a library and a binary (like Lake itself). In such cases, it is common for there to be code (e.g., `main`) that is needed for the binary but should not be included in the library proper.
 * `moreLibTargets`: An `Array` of additional library `FileTarget`s (beyond the package's and its dependencies' libraries) to build and link to the package's binary executable (and/or to dependent package's executables).
+* `supportInterpreter`: Whether to expose symbols within the executable to the Lean interpreter. This allows the executable to interpret Lean files (e.g., via `Lean.Elab.runFrontend`). Implementation-wise, this passes `-rdynamic` to the linker when building on a non-Windows systems. Defaults to `false`.
 * `moreLinkArgs`: An `Array` of additional arguments to pass to `leanc` while compiling the package's binary executable. These will come *after* the paths of libraries built with `moreLibTargets`.
 
 ## Scripts
diff --git a/build.sh b/build.sh
index 759e89e92d..ffde950680 100755
--- a/build.sh
+++ b/build.sh
@@ -1,6 +1,6 @@
 #!/usr/bin/env sh
 if [ "$OS" = "Windows_NT" ]; then
-  LINK_OPTS=-Wl,--export-all
+  LINK_OPTS=
 else
   LINK_OPTS=-rdynamic
 fi
diff --git a/examples/bootstrap/lakefile.lean b/examples/bootstrap/lakefile.lean
index a686b25f91..0c364f5c3d 100644
--- a/examples/bootstrap/lakefile.lean
+++ b/examples/bootstrap/lakefile.lean
@@ -4,8 +4,4 @@ open System Lake DSL
 package lake where
   srcDir := FilePath.mk ".." / ".."
   binRoot := `Lake.Main
-  moreLinkArgs :=
-    if Platform.isWindows then
-      #["-Wl,--export-all"]
-    else
-      #["-rdynamic"]
+  supportInterpreter := true
diff --git a/lakefile.lean b/lakefile.lean
index 4a687ef7a4..1ae9dc5002 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -3,8 +3,4 @@ open System Lake DSL
 
 package lake where
   binRoot := `Lake.Main
-  moreLinkArgs :=
-    if Platform.isWindows then
-      #["-Wl,--export-all"]
-    else
-      #["-rdynamic"]
+  moreLinkArgs := if Platform.isWindows then #[] else #["-rdynamic"]