ref: 7858305a8c2dbdfb5c1f3a3ce9b25966cb906b4a
parent: 25d0c42387033e5b23469691718a30740596ff25
author: Paul Brossier <piem@piem.org>
date: Fri Jul 22 01:27:59 EDT 2016
scripts/get_waf.sh: added simple script to fetch latest waf
--- /dev/null
+++ b/scripts/get_waf.sh
@@ -1,0 +1,10 @@
+#! /bin/sh
+
+set -e
+set -x
+
+WAFURL=https://waf.io/waf-1.8.22
+
+( which wget > /dev/null && wget -qO waf $WAFURL ) || ( which curl > /dev/null && curl $WAFURL > waf )
+
+chmod +x waf