From 9b166d4cf4fdd2a0d3fe94762048453387ecf1eb Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 25 Oct 2021 15:17:49 +0200 Subject: [PATCH] Revert "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 fc6ece76ff..77aa54db2d 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"}, true); + opts = opts.update({"interpreter", "prefer_native"}, false); // switch to `true` for changing built-in parsers used in quotations opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false); #endif