diff --git a/doc/make/index.md b/doc/make/index.md
index 5ad89fff23..2ab06028b1 100644
--- a/doc/make/index.md
+++ b/doc/make/index.md
@@ -180,6 +180,11 @@ affect later stages. This is an issue in two specific cases.
   For an example, see https://github.com/leanprover/lean4/commit/f9dcbbddc48ccab22c7674ba20c5f409823b4cc1#diff-371387aed38bb02bf7761084fd9460e4168ae16d1ffe5de041b47d3ad2d22422
   (from before the flag defaulted to `false`).
   
+To modify either of these flags both for building and editing the stdlib, adjust
+the code in `stage0/src/stdlib_flags.h`. The flags will automatically be reset
+on the next `update-stage0` when the file is overwritten with the original
+version in `src/`.
+
 Development Setup
 -----------------
 
diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix
index c406609d82..9eeea9fc49 100644
--- a/nix/bootstrap.nix
+++ b/nix/bootstrap.nix
@@ -74,7 +74,6 @@ rec {
         src = ../src;
         fullSrc = ../.;
         inherit debug;
-        leanFlags = [ "-Dinterpreter.prefer_native=false" ];
       });
     in (all: all // all.lean) rec {
       Init = build { name = "Init"; deps = []; };
diff --git a/src/library/compiler/ir_interpreter.cpp b/src/library/compiler/ir_interpreter.cpp
index a25556f421..b5eb1c570d 100644
--- a/src/library/compiler/ir_interpreter.cpp
+++ b/src/library/compiler/ir_interpreter.cpp
@@ -48,13 +48,8 @@ functions, which have a (relatively) homogeneous ABI that we can use without run
 #include "util/option_declarations.h"
 
 #ifndef LEAN_DEFAULT_INTERPRETER_PREFER_NATIVE
-#if LEAN_IS_STAGE0 == 1
-// We already set `-Dinterpreter.prefer_native=false` in stdlib.make, but also set it here as a default when we use stage 0 in the editor
-#define LEAN_DEFAULT_INTERPRETER_PREFER_NATIVE false
-#else
 #define LEAN_DEFAULT_INTERPRETER_PREFER_NATIVE true
 #endif
-#endif
 
 namespace lean {
 namespace ir {
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index 459ab0d52b..135a61969d 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -35,6 +35,7 @@ Author: Leonardo de Moura
 #include "initialize/init.h"
 #include "library/compiler/ir_interpreter.h"
 #include "util/path.h"
+#include "stdlib_flags.h"
 #ifdef _MSC_VER
 #include <io.h>
 #define STDOUT_FILENO 1
@@ -429,7 +430,7 @@ int main(int argc, char ** argv) {
         return 1;
     }
 
-    options opts;
+    options opts = get_default_options();
     optional<std::string> server_in;
     std::string native_output;
     optional<std::string> c_output;
diff --git a/src/stdlib.make.in b/src/stdlib.make.in
index 2d87c4acd9..acc59d2615 100644
--- a/src/stdlib.make.in
+++ b/src/stdlib.make.in
@@ -14,7 +14,7 @@ LEANMAKE_OPTS=\
 	LIB_OUT="${LIB}/lean"\
 	OLEAN_OUT="${LIB}/lean"\
 	BIN_OUT="${CMAKE_BINARY_DIR}/bin"\
-	LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS} -Dinterpreter.prefer_native=false"\
+	LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS}"\
 	LEANC_OPTS+="${LEANC_OPTS}"\
 	LEAN_CXX="${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER}"\
 	LEAN_AR="${CMAKE_AR}"\
diff --git a/src/stdlib_flags.h b/src/stdlib_flags.h
new file mode 100644
index 0000000000..37aa19a850
--- /dev/null
+++ b/src/stdlib_flags.h
@@ -0,0 +1,15 @@
+#include "util/options.h"
+
+namespace lean {
+options get_default_options() {
+    options opts;
+    // see https://leanprover.github.io/lean4/doc/make/index.html#further-bootstrapping-complications
+#if LEAN_IS_STAGE0 == 1
+    // switch to `true` for ABI-breaking changes affecting meta code
+    opts.update("interpreter.prefer_native", false);
+    // switch to `true` for changing built-in parsers
+    opts.update("internal.parseQuotWithCurrentStage", false);
+#endif
+    return opts;
+}
+}