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.

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

Include script generated source file #12

Merged
merged 5 commits into from
Jul 22, 2022
Merged

Include script generated source file #12

merged 5 commits into from
Jul 22, 2022

Conversation

mjwen
Copy link
Collaborator

@mjwen mjwen commented Jul 15, 2022

Explicitly include script generated source file in the repo, instead of generating them each time at building.

@yafshar
Copy link
Member

yafshar commented Jul 15, 2022

@mjwen generally sounds great. But let me also take a closer look at the changes before merging

@yafshar
Copy link
Member

yafshar commented Jul 16, 2022

@mjwen thanks, lots of cleaning from ' -> ". I think it was better if you divided them into 2 PR. Anyhow, I think it is great. I did not understand if you plan to keep the generate scripts or, now that you have created all the files, do you plan to remove those scripts?

@mjwen
Copy link
Collaborator Author

mjwen commented Jul 16, 2022

Yeah, I should have split this into to PRs...

The purpose to include the generated files is to make stuff more explicit -- if someone whats to take a look at a specific binging script, it can be then be simply done. Another point is kind of philosophical: the generated files are the main stuff, and the scripts that generate them are only auxiliary. I am definitely not planning to delete the scripts that generate the files.

@mjwen mjwen merged commit a5e0f3a into master Jul 22, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants