Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

build: Update config/default_config.cmake during mach update. #299

Open
Tracked by #12
duesee opened this issue Dec 7, 2022 · 1 comment
Open
Tracked by #12

build: Update config/default_config.cmake during mach update. #299

duesee opened this issue Dec 7, 2022 · 1 comment
Labels
build 🔨

Comments

@duesee
Copy link
Contributor

duesee commented Dec 7, 2022

We (probably) can just copy build/config.cmake to config/default_config.cmake during a mach update.

We could first include a check that compares both files during a default build. If we get confident that this does not introduce friction into our workflows, we could make it the default.
@duesee
Copy link
Contributor Author

duesee commented Dec 12, 2022

@franziskuskiefer franziskuskiefer mentioned this issue Dec 13, 2022
Open
5 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
build 🔨
Projects
HACL Packages
Status: Todo
Milestone
No milestone
Development

No branches or pull requests
1 participant
@duesee