#!/bin/bash
set -e
. scripts.inc
rm -rf dist
for dir in $DEVEL; do
echo $dir
(cd $dir && make clean)
done