Skip to content
This repository has been archived by the owner on Apr 29, 2024. It is now read-only.

Introduce user-only configuration. #238 #268

Merged
merged 3 commits into from
Mar 15, 2024
Merged

Conversation

hadronized
Copy link
Owner

@hadronized hadronized commented Mar 13, 2024

That commit allows to decouple what the user can customize (which is mostly optional), and what we really want to be there (which is requiring almost everything to be provided). That requires being able to merge user configurations with regular configurations, and to create a regular configuration from a user configuration (for instance, when adding a new language config via the user configuration only), which can fail if some options are not provided.

@hadronized hadronized marked this pull request as ready for review March 15, 2024 19:20
That commit allows to decouple what the user can customize (which is mostly optional), and we want really
want to be there (which is requiring almost everything to be provided). That requires being able to merge
user configurations with regular configurations, and to create a regular configuration from a user
configuration (for instance, when adding a new language config via the user configuration only), which can
fail if some options are not provided.
The extra logging (debug) allows to check exactly with which configuration we are running. A full dump of the
configuration is sunk to the logger implementation via a trace! call.
@hadronized hadronized merged commit 9fccddd into master Mar 15, 2024
3 checks passed
@hadronized hadronized deleted the 238-merge-configs branch March 15, 2024 19:25
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

1 participant