[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

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: