diff options
author | dzwdz | 2023-08-14 18:51:07 +0200 |
---|---|---|
committer | dzwdz | 2023-08-14 18:51:07 +0200 |
commit | 642b5fb0007b64c77d186fcb018d571152ee1d47 (patch) | |
tree | 1c466461f3602d306be309a053edae558ef2568e /contrib/dep_builders/dl | |
parent | 8050069c57b729c18c19b1a03ab6e4bf63b4735e (diff) |
reorganization: first steps
Diffstat (limited to 'contrib/dep_builders/dl')
-rwxr-xr-x | contrib/dep_builders/dl | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/contrib/dep_builders/dl b/contrib/dep_builders/dl new file mode 100755 index 0000000..e6f279f --- /dev/null +++ b/contrib/dep_builders/dl @@ -0,0 +1,9 @@ +#!/bin/sh +# downloads a file to toolchain/cache unless it's already present there + +mkdir -p cache/toolchain +OUT="cache/toolchain/$(basename $1)" + +[ -e "$OUT" ] && exit +echo "downloading $1..." +curl "$1" > $OUT |