Improve FLINT autogen README
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 in sage_setup?) but that shouldn't conflict with this PR.
Thanks for improving the flint auto-generation. I will have a look.
I don't quite understand the point of the flint-commit.txt file. It is an extra burden to maintain. If you feel like the information is relevant, I would modify the script so that the (short) commit hash number is written inside each auto-generated file.
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.
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 61674fd891a44e1d3c13fc3c68a1bc68aa441aef; changes) is ready! :tada: This preview will update shortly after each push to this PR.