Bug#589999: coq: FTBFS on sparc: test failure
Le 22/07/2010 22:59, Cyril Brulebois a écrit :
> | if grep -F 'Error!' test-suite/summary.log ; then false; fi
> | success/Nsatz.v...Error! (should be accepted)
> | success/Nsatz_domain.v...Error! (should be accepted)
> | bugs/closed/shouldsucceed/2145.v...Error! (bug seems to be opened, please check)
> | micromega/bertot.v...Error! (should be accepted)
> | micromega/example.v...Error! (should be accepted)
> | micromega/qexample.v...Error! (should be accepted)
> | micromega/rexample.v...Error! (should be accepted)
> | micromega/square.v...Error! (should be accepted)
> | micromega/zomicron.v...Error! (should be accepted)
> | make[3]: *** [test-suite] Error 1
> | make[3]: Leaving directory `/build/buildd-coq_8.3~beta0+13298-1-sparc-do5ShS/coq-8.3~beta0+13298'
> | make[2]: *** [check] Error 2
This is most likely #570920. Since this bug is already fixed in ocaml
3.12, I'll wait for whichever of coq 8.3 or ocaml 3.12 hits first
unstable (both are still in beta stages) before any further action.
Cheers,
--
Stéphane
Reply to: