Skip to content

Commit 43b5d0d

Browse files
authored
try prefer_native
1 parent ec0bf8c commit 43b5d0d

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

stage0/src/stdlib_flags.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ options get_default_options() {
66
// see https://lean-lang.org/lean4/doc/dev/bootstrap.html#further-bootstrapping-complications
77
#if LEAN_IS_STAGE0 == 1
88
// switch to `true` for ABI-breaking changes affecting meta code
9-
opts = opts.update({"interpreter", "prefer_native"}, false);
9+
opts = opts.update({"interpreter", "prefer_native"}, true);
1010
// switch to `true` for changing built-in parsers used in quotations
1111
opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
1212
// toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax

0 commit comments

Comments
 (0)