Closed dinosaure closed 2 years ago
is the addition of bench/main.html in this PR intentional?
I'm not sure about that. I would like to say yes because it's a standalone benchmark of checkseum
which permits to show performances of it and I would like to say no because it's a huge file.
I finally deleted the bench/main.html
and the compilation of the benchmark (which should be done via dune build --profile benchmark
now).
I check by hands tests on 4.11.2+32bit
, it should be fine on 32bit architectures.
is the addition of bench/main.html in this PR intentional?