diff options
Diffstat (limited to 'configure')
-rwxr-xr-x | configure | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -844,6 +844,7 @@ fi if [ "$arch" = "riscV" ] ; then cat >> Makefile.config <<EOF +EXTRA_EXTRACTION=Asm.ireg_eq Asm.ireg0_eq BACKENDLIB=Asmgenproof0.v Asmgenproof1.v ExtValues.v EOF fi |