#!/bin/bash
set -eu

echo

# check configure files here, if necessary

echo "Running make" "$@"

make "$@"

echo
echo "Compilation finished successfully."
echo