From 6efb459d5b103fe5e7d772ecc0fbeb62b880dc7c Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 25 Oct 2021 12:52:06 +0200 Subject: [PATCH] chore: prefer native --- src/stdlib_flags.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/stdlib_flags.h b/src/stdlib_flags.h index 77aa54db2d..fc6ece76ff 100644 --- a/src/stdlib_flags.h +++ b/src/stdlib_flags.h @@ -6,7 +6,7 @@ options get_default_options() { // 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 = opts.update({"interpreter", "prefer_native"}, false); + opts = opts.update({"interpreter", "prefer_native"}, true); // switch to `true` for changing built-in parsers used in quotations opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false); #endif