Meta/Make: pass --no-prove and --long down thru Dothem to Make

diff --git a/Dothem b/Dothem
index 8dca9ce947db46cb674d4f5c59646e121360810c..c5d4c387ff5e5504281748f1cd70628fe144767e 100755 (executable)
--- a/Dothem
+++ b/Dothem
@@ -16,12 +16,13 @@ inst_prefix=$(
        echo $HOME
 )
 
-force= with_dash= M= install= nodoc= notest= bootstrap= branches= jobs=
-scratch=
+force= with_dash= test_long= M= install= nodoc= notest= bootstrap= branches= jobs=
+scratch= noprove=
 while  case "$1" in
        --pedantic | --locale=* | --loose) M="$M $1" ;;
        --force) force=$1 ;;
        --dash) with_dash=y ;;
+       --long) test_long=--long ;;
        --noinstall) install=noinstall ;;
        --nodoc) nodoc=y ;;
        --notest) notest=y ;;
@@ -30,6 +31,7 @@ while case "$1" in
        --bootstrap) bootstrap=y ;;
        --base=*) BUILDBASE=${1#*=} ;;
        --branches=*) branches=${1#*=} ;;
+       --noprove) noprove=$1 ;;
        -j*) jobs=$1 ;;
        --) shift; break ;;
        -*) echo >&2 "Unknown option: $1"; exit 1 ;;
@@ -194,7 +196,7 @@ do
 
                save=$(git rev-parse HEAD) &&
 
-               Meta/Make $M ${test+"$test"} $jobs --memtrash \
+               Meta/Make $M $noprove ${test+"$test"} $jobs $test_long --memtrash \
                    -- ${with_dash:+SHELL_PATH=/bin/dash} "$@" $dotest &&
 
                {

diff --git a/Make b/Make
index 0e422e20323b65368867b042197dd599338ff5a3..3ea1d24bdb262cde8d4e03677adad1e9bbcdfc86 100755 (executable)
--- a/Make
+++ b/Make
@@ -149,6 +149,10 @@ do
                        done | tr '\012' ' '
                )
                ;;
+       --long)
+               GIT_TEST_LONG=YesPlease
+               export GIT_TEST_LONG
+               ;;
        --dash)
                with_dash=y
                ;;