#!/bin/bash

set -e

. scripts.inc

for dir in $DEVEL; do
  echo $dir
  (cd $dir && make build BUILDFLAGS="$BUILDFLAGS")
done