Add testcase for #461

2 jobs for !798 with paolo/fix-461 in 6 minutes and 24 seconds
merge request
Name Stage Failure
failed
build-coq.8.13.2 Build
make[2]: Target 'real-all' not remade because of errors.
make[1]: *** [Makefile.coq:343: all] Error 2
make: *** [Makefile:3: all] Error 2

real 4m24.953s
user 17m4.838s
sys 1m20.233s
Cleaning up project directory and file based variables
ERROR: Job failed: exit code 1

failed
build-coq.8.14.1-mr Build
make[2]: Target 'real-all' not remade because of errors.
make[1]: *** [Makefile.coq:386: all] Error 2
make: *** [Makefile:3: all] Error 2

real 4m18.289s
user 17m24.149s
sys 1m20.201s
Cleaning up project directory and file based variables
ERROR: Job failed: exit code 1