-
-
Notifications
You must be signed in to change notification settings - Fork 482
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
Improve FLINT autogen README #37458
Improve FLINT autogen README #37458
Conversation
Thanks for improving the flint auto-generation. I will have a look. |
I don't quite understand the point of the And in practice, it does not quite work this way. Typically, one has to modify flint sources so that the auto-generation works properly. |
Thanks for the response, the idea is that someone else should be able to reproduce the autogenerated headers on their machine too, and since e.g. for v3.0.1 a commit different from the release tag is used, it should be noted somewhere. I tried another approach, can you take a look? It puts the git commit line at the top of the generated files :) |
Better this way I would say. |
7638b1b
to
a7314cb
Compare
Sorry there’s a small linting issue, I will fix it when I get back. @grhkm21 |
Not sure why it got triggered, but the fix from https://stackoverflow.com/questions/30454549/a-literal-in-restructuredtext works. I assume this is still a positive review, feel free to revert if you disagree with the one-char change |
merge conflict |
Documentation preview for this PR (built with commit 61674fd; changes) is ready! 🎉 |
The FLINT headers are generated manually using a script from #36449. However, the documentations are not quite clear, and neither is the commit that the current headers are generated from. This commit adds these two details.
@videlec do you mind reviewing? I am not sure if the
flint-commit.txt
is an acceptable way to put this information, or where I should put it. Also I'm aware that this script might be moved in the future (since it shouldn't belong insage_setup
?) but that shouldn't conflict with this PR.