diff --git a/gnu/dist/fetch.sh b/gnu/dist/fetch.sh new file mode 100644 index 000000000..9d41b5369 --- /dev/null +++ b/gnu/dist/fetch.sh @@ -0,0 +1,18 @@ +#!/bin/sh + +# Make sure we're in our directory (i.e., where this shell script is) +echo $0 +cd `dirname $0` + +# Fetch sources if not available +if [ ! -d gmake ]; +then + if [ ! -f make-3.80.tar.bz2 ]; + then + wget ftp://ftp.gnu.org/gnu/make/make-3.80.tar.bz2 + fi + + tar -xf make-3.80.tar.bz2 && \ + mv make-3.80 gmake +fi +