scripts/get_waf.sh: add script to fetch latest waf
authorPaul Brossier <piem@piem.org>
Thu, 21 Jul 2016 21:02:08 +0000 (23:02 +0200)
committerPaul Brossier <piem@piem.org>
Thu, 21 Jul 2016 21:02:08 +0000 (23:02 +0200)
scripts/get_waf.sh [new file with mode: 0755]

diff --git a/scripts/get_waf.sh b/scripts/get_waf.sh
new file mode 100755 (executable)
index 0000000..e2fbd16
--- /dev/null
@@ -0,0 +1,10 @@
+#! /bin/sh
+
+set -e
+set -x
+
+WAFURL=https://waf.io/waf-1.9.1
+
+( which wget > /dev/null && wget -qO waf $WAFURL ) || ( which curl > /dev/null && curl $WAFURL > waf )
+
+chmod +x waf