Meta/Dothem: --dash option builds only with dash

Earlier one tried to build with /bin/sh and /bin/dash but to do so correctly
we need to 'make clean' in the middle, which is too much overhead to do many
times a day.

diff --git a/Dothem b/Dothem
index 3106a30b288f763c67fd80e9f37c4b17d0df0320..418ec050ce836b55c3a0af06a82b4195aeb292d9 100755 (executable)
--- a/Dothem
+++ b/Dothem
@@ -148,18 +148,13 @@ do
 
                save=$(git rev-parse HEAD) &&
 
-               {
-                       test "z$with_dash" != 'zy' ||
-                       Meta/Make $M ${test+"$test"} -- $jobs SHELL_PATH=/bin/dash $dotest
-               } &&
-
-               Meta/Make $M ${test+"$test"} -- $jobs $dotest &&
+               Meta/Make $M ${test+"$test"} $jobs -- ${with_dash:+SHELL_PATH=/bin/dash} $dotest &&
 
                {
                        test -n "$nodoc" ||
                        if test "$save" = "$(git rev-parse HEAD)"
                        then
-                               Meta/Make $M -- $jobs doc &&
+                               Meta/Make $M $jobs -- doc &&
                                Meta/Make $M -- install-man install-html
                        else
                                echo >&2 "Head moved--not installing docs"
@@ -177,6 +172,6 @@ do
                } || exit $?
 
                git reset --hard
-       ) || break;
+       ) </dev/null || exit $?
 
 done