diff --git a/Doit b/Doit index 74051e02d7..1d4c4d64ad 100755 --- a/Doit +++ b/Doit @@ -6,6 +6,7 @@ while case "$1" in -pedantic) M=$1 ;; -force) force=$1 ;; -dash) with_dash=y ;; + -noinstall) install=noinstall ;; *) break ;; esac do @@ -91,7 +92,10 @@ do *) : ;; esac && - Meta/Make $M -- install && + { + test z$install = znoinstall || + Meta/Make $M -- install + } && Meta/Make clean || exit $? git reset --hard