Skip to content

Commit

Permalink
chore: update stage0
Browse files Browse the repository at this point in the history
  • Loading branch information
mhuisi committed Nov 15, 2024
1 parent c23a3ae commit bc8d566
Show file tree
Hide file tree
Showing 120 changed files with 135,404 additions and 119,511 deletions.
11 changes: 10 additions & 1 deletion stage0/src/include/lean/lean.h

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
6 changes: 5 additions & 1 deletion stage0/stdlib/Init/Data/Array.c

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

187 changes: 187 additions & 0 deletions stage0/stdlib/Init/Data/Array/Monadic.c

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

29 changes: 0 additions & 29 deletions stage0/stdlib/Init/Data/Array/Subarray.c

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

Loading

0 comments on commit bc8d566

Please sign in to comment.