#!/bin/sh
(cd tools && ./configure "$@")
