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 61674fd; changes) is ready! 🎉
This preview will update shortly after each push to this PR.