1 files changed, 9 insertions, 0 deletions
diff --git a/tools/dep_builders/dl b/tools/dep_builders/dl
new file mode 100755
index 0000000..8cfeebc
--- /dev/null
+++ b/tools/dep_builders/dl
@@ -0,0 +1,9 @@
+#!/bin/sh
+# downloads a file to toolchain/cache unless it's already present there
+
+mkdir -p toolchain/cache
+OUT="toolchain/cache/$(basename $1)"
+
+[ -e "$OUT" ] && exit
+echo "downloading $1..."
+curl "$1" > $OUT