mirror of
https://github.com/git/git.git
synced 2026-07-04 21:58:19 +00:00
$DESTDIR is more usual during the build than $dest and is what is usually used in the makefiles, so let's use it too. Signed-off-by: Petr Baudis <pasky@ucw.cz> Signed-off-by: Junio C Hamano <junkio@cox.net>