Merge branch 'master' of

2 jobs for !275 with master in 9 minutes and 58 seconds (queued for 3 seconds)
merge request
Name Stage Failure
build-coq.8.13.2-mr Build
make[1]: *** [all] Error 2
Makefile:3: recipe for target 'all' failed
make: *** [all] Error 2

real 0m30.500s
user 0m32.840s
sys 0m5.516s
Cleaning up file based variables
ERROR: Job failed: exit code 1