scripts/get_waf.sh

   1 #! /bin/sh
   2
   3 set -e
   4 set -x
   5
   6 WAFURL=https://waf.io/waf-1.8.22
   7
   8 ( which wget > /dev/null && wget -qO waf $WAFURL ) || ( which curl > /dev/null && curl $WAFURL > waf )
   9
  10 chmod +x waf