#!/bin/sh

echo "This script is deprecated. Next time, run \"make tools\" instead."
make tools