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