Meta/Dothem: make --memtrash configurable

diff --git a/Dothem b/Dothem
index c5d4c387ff5e5504281748f1cd70628fe144767e..ce467d74177e1cd72b6ba5fe1282ea60a16900a0 100755 (executable)
--- a/Dothem
+++ b/Dothem
@@ -17,7 +17,7 @@ inst_prefix=$(
 )
 
 force= with_dash= test_long= M= install= nodoc= notest= bootstrap= branches= jobs=
-scratch= noprove=
+scratch= noprove= memtrash=--memtrash
 while  case "$1" in
        --pedantic | --locale=* | --loose) M="$M $1" ;;
        --force) force=$1 ;;
@@ -26,6 +26,8 @@ while case "$1" in
        --noinstall) install=noinstall ;;
        --nodoc) nodoc=y ;;
        --notest) notest=y ;;
+       --nomemtrash) memtrash= ;;
+       --memtrash) memtrash=--memtrash ;;
        --test=*) test="$1" ;;
        --scratch) scratch=y ;;
        --bootstrap) bootstrap=y ;;
@@ -196,7 +198,7 @@ do
 
                save=$(git rev-parse HEAD) &&
 
-               Meta/Make $M $noprove ${test+"$test"} $jobs $test_long --memtrash \
+               Meta/Make $M $noprove ${test+"$test"} $jobs $test_long $memtrash \
                    -- ${with_dash:+SHELL_PATH=/bin/dash} "$@" $dotest &&
 
                {