Diff

Differences From Artifact [1464904b80]:

To Artifact [d2befa5f72]:


61
62
63
64
65
66
67














68
69
70
71
72
73
74
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88







+
+
+
+
+
+
+
+
+
+
+
+
+
+







		fi
	done

	rm -rf out

	exit 0
}

function not_platforms_regexp () {
	local platform_re

	for platform_re in "$@"; do
		if echo "${PLATFORM}" | grep -- "${platform_re}" >/dev/null; then
			rm -rf out

			exit 0
		fi
	done

	return 0
}

function download () {
	local url file

	file="$1"
	url="$2"