Skip to content

Commit

Permalink
chore: update stage0
Browse files Browse the repository at this point in the history
  • Loading branch information
Lean stage0 autoupdater committed Nov 1, 2024
1 parent 1f8d756 commit 3f33cd6
Show file tree
Hide file tree
Showing 51 changed files with 12,383 additions and 11,666 deletions.
5 changes: 3 additions & 2 deletions stage0/src/library/module.cpp

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion stage0/src/stdlib_flags.h
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ options get_default_options() {
// switch to `true` for ABI-breaking changes affecting meta code
opts = opts.update({"interpreter", "prefer_native"}, false);
// switch to `true` for changing built-in parsers used in quotations
opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
// toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax
// with custom precheck hooks were affected
opts = opts.update({"quotPrecheck"}, true);
Expand Down
544 changes: 272 additions & 272 deletions stage0/stdlib/Lake/Build/Actions.c

Large diffs are not rendered by default.

4 changes: 2 additions & 2 deletions stage0/stdlib/Lake/Util/Log.c

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

24 changes: 12 additions & 12 deletions stage0/stdlib/Lean/Data/Lsp/Capabilities.c

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

10 changes: 5 additions & 5 deletions stage0/stdlib/Lean/Data/Lsp/CodeActions.c

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

Loading

0 comments on commit 3f33cd6

Please sign in to comment.