development/git
development/git
1
0
Fork 0
mirror of https://github.com/git/git synced 2024-11-05 18:59:29 +00:00
Code Issues Projects Releases Packages Wiki Activity

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

Browse source 
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.
This commit is contained in:
Junio C Hamano 2010-01-31 18:26:36 -08:00
parent 96d720e449
commit 85ace14c2b
1 changed files with 3 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
Dothem
View file

@ -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