Albin Ahlbäck
Albin Ahlbäck
Thanks for noticing this! Looks like we should remove the one in `double_interval.h` as it is currently unused, but I'll let @fredrik-johansson decide when he gets back from vacation.
Sorry, I will fix it this weekend.
Will fix after #2085 is merged (or closed). I would like to avoid conflicts.
Not yet, but I'll add it to the list of issues for the workshop next month.
I gave a thumbs up for the thought and discussion. I'm not sure whether I like the idea.
It looks like https://github.com/Nemocas/Nemo.jl/pull/1994 is the cause of this. To test this, just run `flint/nmod-test.jl`.
They must have something to merge files, no?
I'm sure I am misunderstanding something; you would like to disable merging of files for MinGW, that one system that actually requires it in order compile FLINT?
I have thought about this for a little bit, and I do not think this is an issue about FLINT. I believe this is a pretty standard feature of linkers,...
I think a redirect is suitable. For reference, one can just put ```html ``` in the header, which should work for all modern browsers. Arb, Calcium and GR should also...