Unverified Commit 5e849c77 authored by Tommaso Tocci's avatar Tommaso Tocci
Browse files

bugfix: (download script) ensure folder creation

Source folder was removed if existed before but never recreated
parent e9beac80
Loading
Loading
Loading
Loading
+1 −2
Original line number Diff line number Diff line
@@ -35,9 +35,8 @@ wgetdeps() {
    URL=$2
    if [ -d "${SOURCE}/${FOLDER}" ]; then
        rm -rf "${SOURCE}/${FOLDER}"
    else
        mkdir -p "${SOURCE}/${FOLDER}"
    fi
    mkdir -p "${SOURCE}/${FOLDER}"
    cd ${SOURCE}
    FILENAME=$(basename $URL)
    if [ -f "${SOURCE}/$FILENAME" ]; then