diff -r f75f5b3bc14f -r e05f3e8ec2cb test/configure --- a/test/configure Sat Nov 14 21:12:53 2020 +0100 +++ b/test/configure Sun Apr 16 14:16:31 2023 +0200 @@ -81,10 +81,10 @@ "--includedir="*) INCLUDEDIR=${ARG#--includedir=} ;; "--infodir="*) INFODIR=${ARG#--infodir=} ;; "--mandir"*) MANDIR=${ARG#--mandir} ;; - "--help"*) printhelp; exit 1 ;; + "--help"*) printhelp; rm -Rf $TEMP_DIR; exit 1 ;; "--enable-pg") FEATURE_PG=on ;; "--disable-pg") unset FEATURE_PG ;; - "-"*) echo "unknown option: $ARG"; exit 1 ;; + "-"*) echo "unknown option: $ARG"; rm -Rf $TEMP_DIR; exit 1 ;; esac done